Hoogle Search
Within LTS Haskell 24.6 (ghc-9.10.2)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
-
sbv Documentation.SBV.Examples.KnuckleDragger.Lists In general, mapping and filtering operations do not commute. We'll see the kind of counter-example we get from SBV if we attempt to prove:
>>> mapFilter `catch` (\(_ :: SomeException) -> pure ()) Lemma: badMapFilter *** Failed to prove badMapFilter. Falsifiable. Counter-example: xs = [A_3] :: [A] lhs = [A_0] :: [A] rhs = [] :: [A] f :: A -> A f _ = A_0 p :: A -> Bool p A_3 = True p _ = False
As expected, the function f maps everything to A_0, and the predicate p only lets A_3 through. As shown in the counter-example, for the input [A_3], left-hand-side filters nothing and the result is the singleton A_0. But the map on the right-hand side maps everything to [A_0] and the filter gets rid of the elements, resulting in an empty list. -
sbv Documentation.SBV.Examples.KnuckleDragger.Lists map f . reverse == reverse . map f
>>> mapReverse Inductive lemma: mapAppend Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Step: 5 Q.E.D. Result: Q.E.D. Inductive lemma: mapReverse Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Step: 5 Q.E.D. Step: 6 Q.E.D. Result: Q.E.D. [Proven] mapReverse
-
sbv Documentation.SBV.Examples.KnuckleDragger.Lists length xs = length ys ⟹ map fst (zip xs ys) = xs
>>> map_fst_zip Inductive lemma: map_fst_zip Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Result: Q.E.D. [Proven] map_fst_zip
-
sbv Documentation.SBV.Examples.KnuckleDragger.Lists map fst (zip xs ys) = take (min (length xs) (length ys)) xs
>>> map_fst_zip_take Lemma: take_cons Q.E.D. Inductive lemma: map_fst_zip_take Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Step: 5 Q.E.D. Result: Q.E.D. [Proven] map_fst_zip_take
-
sbv Documentation.SBV.Examples.KnuckleDragger.Lists length xs = length ys ⟹ map snd (zip xs ys) = xs
>>> map_snd_zip Inductive lemma: map_snd_zip Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Result: Q.E.D. [Proven] map_snd_zip
-
sbv Documentation.SBV.Examples.KnuckleDragger.Lists map snd (zip xs ys) = take (min (length xs) (length ys)) xs
>>> map_snd_zip_take Lemma: take_cons Q.E.D. Inductive lemma: map_snd_zip_take Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Step: 5 Q.E.D. Result: Q.E.D. [Proven] map_snd_zip_take
mapM :: Monad m => (b -> m c) -> Fold m a b -> Fold m a cstreamly-core Streamly.Data.Fold Deprecated: Use rmapM instead
mapMaybe :: forall (m :: Type -> Type) a b r . Monad m => (a -> Maybe b) -> Fold m b r -> Fold m a rstreamly-core Streamly.Data.Fold mapMaybe f fold maps a Maybe returning function f on the input of the fold, filters out Nothing elements, and return the values extracted from Just.
>>> mapMaybe f = Fold.lmap f . Fold.catMaybes >>> mapMaybe f = Fold.mapMaybeM (return . f)
>>> f x = if even x then Just x else Nothing >>> fld = Fold.mapMaybe f Fold.toList >>> Stream.fold fld (Stream.enumerateFromTo 1 10) [2,4,6,8,10]
mapM :: Monad m => (a -> m b) -> Stream m a -> Stream m bstreamly-core Streamly.Data.Stream >>> mapM f = Stream.sequence . fmap f
Apply a monadic function to each element of the stream and replace it with the output of the resulting action.>>> s = Stream.fromList ["a", "b", "c"] >>> Stream.fold Fold.drain $ Stream.mapM putStr s abc
mapMaybe :: forall (m :: Type -> Type) a b . Monad m => (a -> Maybe b) -> Stream m a -> Stream m bstreamly-core Streamly.Data.Stream Map a Maybe returning function to a stream, filter out the Nothing elements, and return a stream of values extracted from Just. Equivalent to:
>>> mapMaybe f = Stream.catMaybes . fmap f