Hoogle Search

Within LTS Haskell 24.34 (ghc-9.10.3)

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

  1. mapCV2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> (FP -> FP -> FP) -> (Rational -> Rational -> Rational) -> CV -> CV -> CV

    sbv Data.SBV.Internals

    Map a binary function through a CV.

  2. map2 :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b -> SBV c) -> SMaybe a -> SMaybe b -> SMaybe c

    sbv Data.SBV.Maybe

    Map over two maybe values.

  3. mapAppend :: (SA -> SB) -> IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Lists 

    map f (xs ++ ys) == map f xs ++ map f ys

    >>> mapAppend (uninterpret "f")
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.
[Proven] mapAppend

  4. mapEquiv :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Lists 

    f = g => map f xs = map g xs

    >>> mapEquiv
Inductive lemma: mapEquiv
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] mapEquiv

  5. mapFilter :: IO ()

    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.

  6. mapReverse :: IO Proof

    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

  7. map_fst_zip :: IO Proof

    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

  8. map_fst_zip_take :: IO Proof

    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

  9. map_snd_zip :: IO Proof

    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

  10. map_snd_zip_take :: IO Proof

    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

Page 299 of many | Previous | Next