Hoogle Search

Within LTS Haskell 24.46 (ghc-9.10.3)

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

  1. sumProof :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Numeric

    Prove that sum of numbers from 0 to n is n*(n-1)/2. 

    >>> sumProof
Inductive lemma: sum_correct
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Result:                               Q.E.D.
[Proven] sum_correct

  2. sumSquareProof :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Numeric

    Prove that sum of square of numbers from 0 to n is n*(n+1)*(2n+1)/6. 

    >>> sumSquareProof
Inductive lemma: sumSquare_correct
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Result:                               Q.E.D.
[Proven] sumSquare_correct

  3. sumToN :: SInteger -> SInteger

    sbv Documentation.SBV.Examples.Misc.Definitions

    Sum of numbers from 0 to the given number. Since this is a recursive definition, we cannot simply symbolically simulate it as it wouldn't terminat. So, we use the function generation facilities to define it directly in SMTLib. Note how the function itself takes a "recursive version" of itself, and all recursive calls are made with this name.

  4. sumToNExample :: IO SatResult

    sbv Documentation.SBV.Examples.Misc.Definitions

    Prove that sumToN works as expected. We have: 

    >>> sumToNExample
Satisfiable. Model:
s0 =  5 :: Integer
s1 = 15 :: Integer

  5. sumCorrect :: IO (InductionResult (S Integer))

    sbv Documentation.SBV.Examples.ProofTools.Sum

    Encoding partial correctness of the sum algorithm. We have: 

    >>> sumCorrect
Q.E.D.

  6. sumTree :: Num a => Tree a -> a

    tree-fun Math.TreeFun.Tree

    Get the sum of a tree for a tree with numbered labels

  7. sumAbsValue :: forall (f :: BaseType -> Type) (sr :: SemiRing) . OrdF f => WeightedSum f sr -> AbstractValue (SemiRingBase sr)

    what4 What4.Expr.WeightedSum

    No documentation available.

  8. sumOffset :: forall (f1 :: BaseType -> Type) (sr :: SemiRing) f2 . Functor f2 => (Coefficient sr -> f2 (Coefficient sr)) -> WeightedSum f1 sr -> f2 (WeightedSum f1 sr)

    what4 What4.Expr.WeightedSum

    Retrieve the constant addend of the weighted sum.

  9. sumRepr :: WeightedSum f sr -> SemiRingRepr sr

    what4 What4.Expr.WeightedSum

    Runtime representation of the semiring for this sum.

  10. sumExpr :: SupportTermOps v => [v] -> v

    what4 What4.Protocol.SMTWriter

    Add a list of values together.

Page 59 of many | Previous | Next