Hoogle Search

Within LTS Haskell 24.10 (ghc-9.10.2)

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

  1. module Language.Fixpoint.Types.Graduals

    This module contains the top-level SOLUTION data types, including various indices used for solving.

  2. class Gradual a

    liquid-fixpoint Language.Fixpoint.Types.Graduals

    Substitute Gradual Solution ---------------------------------------------

  3. class HasGradual a

    liquid-fixpoint Language.Fixpoint.Types.Refinements

    No documentation available.

  4. isGradual :: HasGradual a => a -> Bool

    liquid-fixpoint Language.Fixpoint.Types.Refinements

    No documentation available.

  5. resultGradual :: GSolution -> HashMap KVar (Expr, [Expr])

    liquid-fixpoint Language.Fixpoint.Types.Solutions

    No documentation available.

  6. gradual :: Config -> Bool

    liquidhaskell-boot Language.Haskell.Liquid.UX.Config

    enable gradual type checking

  7. Opt_AutoSccsOnIndividualCafs :: GeneralFlag

    liquidhaskell-boot Liquid.GHC.API

    No documentation available.

  8. individually :: forall (m :: Type -> Type) g f x . (Monad m, Functor g) => Setter (FreeT f m x) (FreeT g m x) (f (FreeT f m x)) (g (FreeT f m x))

    pipes-group Pipes.Group

    Lens to transform each individual functor layer of a FreeT. (over individually) is equivalent to maps, but with a less general type. 

    type Group a m x = Producer a m (Groups a m x)

set  individually :: Monad m => Group a m x -> Transformation a m x
over individually :: Monad m => (Group a m x -> Group a m x) -> Transformation a m x

  9. foldrFoldlDuality :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Lists 

    foldr f e xs == foldl (flip f) e (reverse xs)
    We have: 
    >>> foldrFoldlDuality
Inductive lemma: foldlOverAppend
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Result:                               Q.E.D.
Inductive lemma: foldrFoldlDuality
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] foldrFoldlDuality

  10. foldrFoldlDualityGeneralized :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Lists

    Given: 

    x @ (y @ z) = (x @ y) @ z     (associativity of @)
and e @ x = x                     (left unit)
and x @ e = x                     (right unit)
    Prove: 
    foldr (@) e xs = foldl (@) e xs
    We have: 
    >>> foldrFoldlDualityGeneralized
Inductive lemma: helper
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.
Inductive lemma: foldrFoldlDuality
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] foldrFoldlDuality

Page 20 of many | Previous | Next