Hoogle Search

Within LTS Haskell 24.28 (ghc-9.10.3)

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

  1. mapF :: forall k c (g :: k -> k) (ϕ :: Row (k -> Type)) (ρ :: Row k) . BiForall ϕ ρ c => (forall (h :: k -> Type) (a :: k) . c h a => h a -> h (g a)) -> Rec (Ap ϕ ρ) -> Rec (Ap ϕ (Map g ρ))

    row-types Data.Row.Records

    A function to map over a Ap record given constraints.

  2. map' :: forall f (r :: Row Type) . FreeForall r => (forall a . () => a -> f a) -> Var r -> Var (Map f r)

    row-types Data.Row.Variants

    A function to map over a variant given no constraint.

  3. mapCV :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> (FP -> FP) -> (Rational -> Rational) -> CV -> CV

    sbv Data.SBV.Internals

    Map a unary function through a CV.

  4. 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.

  5. 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.

  6. 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

  7. 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

  8. 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.

  9. 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

  10. 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

Page 258 of many | Previous | Next