Hoogle Search

Within LTS Haskell 24.45 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

  1. bimap :: (SymVal a, SymVal b, SymVal c, SymVal d) => (SBV a -> SBV b) -> (SBV c -> SBV d) -> SEither a c -> SEither b d

    sbv Data.SBV.Either

    Map over both sides of a symbolic Either at the same time 

    >>> let f = uninterpret "f" :: SInteger -> SInteger

>>> let g = uninterpret "g" :: SInteger -> SInteger

>>> prove $ \x -> fromLeft (bimap f g (sLeft x)) .== f x
Q.E.D.

>>> prove $ \x -> fromRight (bimap f g (sRight x)) .== g x
Q.E.D.

  2. SBVMap :: Kind -> Kind -> SMTLambda -> SeqOp

    sbv Data.SBV.Internals

    map a b fun. Where fun :: a -> b, and map :: (a -> b) -> [a] -> [b]

  3. concatMap :: (SymVal a, SymVal b) => (SBV a -> SList b) -> SList a -> SList b

    sbv Data.SBV.List

    concatMap f xs maps f over elements and concats the result.

  4. drop_map :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Lists 

    drop n (map f xs) == map f (drop n xs)

    >>> drop_map
Lemma: drop_cons                        Q.E.D.
Lemma: drop_cons                        Q.E.D.
Lemma: drop_map.n <= 0                  Q.E.D.
Inductive lemma: drop_map.n > 0
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.
Lemma: drop_map
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] drop_map

  5. foldrMapFusion :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Lists 

    foldr f a . map g = foldr (f . g) a
    We have: 
    >>> foldrMapFusion
Inductive lemma: foldrMapFusion
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] foldrMapFusion

  6. take_map :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Lists 

    take n (map f xs) == map f (take n xs)

    >>> take_map
Lemma: take_cons                        Q.E.D.
Lemma: map1                             Q.E.D.
Lemma: take_map.n <= 0                  Q.E.D.
Inductive lemma: take_map.n > 0
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.
Lemma: take_map                         Q.E.D.
[Proven] take_map

  7. tmapEvery :: forall a (cs :: [Type -> Constraint]) p p'' (xs :: [Type]) . TMap (Every cs) xs => p cs -> (forall x (p' :: Type -> Type) . Every cs x => p' x -> a) -> p'' xs -> [a]

    servant-openapi3 Servant.OpenApi.Internal.TypeLevel.Every

    Like tmap, but uses Every for multiple constraints. 

    >>> let zero :: forall p a. (Show a, Num a) => p a -> String; zero _ = show (0 :: a)

>>> tmapEvery (Proxy :: Proxy [Show, Num]) zero (Proxy :: Proxy [Int, Float]) :: [String]
["0","0.0"]

  8. module Servant.OpenApi.Internal.TypeLevel.TMap

    No documentation available.

  9. class TMap (q :: k -> Constraint) (xs :: [k])

    servant-openapi3 Servant.OpenApi.Internal.TypeLevel.TMap

    Map a list of constrained types to a list of values. 

    >>> tmap (Proxy :: Proxy KnownSymbol) symbolVal (Proxy :: Proxy ["hello", "world"])
["hello","world"]

  10. tmap :: TMap q xs => p q -> (forall (x :: k) (p' :: k -> Type) . q x => p' x -> a) -> p'' xs -> [a]

    servant-openapi3 Servant.OpenApi.Internal.TypeLevel.TMap

    No documentation available.

Page 1084 of many | Previous | Next