sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- !
- #
- %
- *
- +
- .
- /
- =
- \
- ^
- |
- -
- _
- All

Index - F

F |
1 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours
2 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Fib
f |
1 (Function) | Documentation.SBV.Examples.Uninterpreted.AUF
2 (Function) | Documentation.SBV.Examples.Uninterpreted.Function
3 (Function) | Documentation.SBV.Examples.Uninterpreted.Sort
F1 | Documentation.SBV.Examples.BitPrecise.Legato
F2 | Documentation.SBV.Examples.BitPrecise.Legato
Factorial | Documentation.SBV.Examples.Queries.FourFours
Failed |
1 (Data Constructor) | Data.SBV.Tools.WeakestPreconditions
2 (Data Constructor) | Data.SBV.Tools.Induction
falseCV | Data.SBV.Internals
falseSV | Data.SBV.Internals
Falsity | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
fastMaxCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
fastMinCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
fastPopCountIsCorrect | Documentation.SBV.Examples.CodeGeneration.PopulationCount
Female | Documentation.SBV.Examples.Puzzles.Murder
fib | Documentation.SBV.Examples.WeakestPreconditions.Fib
fib0 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
fib1 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
fib2 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
fibCorrect | Documentation.SBV.Examples.ProofTools.Fibonacci
FibS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Fib
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Fib
fill | Documentation.SBV.Examples.Queries.FourFours
fillBoard | Documentation.SBV.Examples.Puzzles.Sudoku
filter | Data.SBV.List
find | Documentation.SBV.Examples.Queries.FourFours
findDays | Documentation.SBV.Examples.Queries.Enums
findHD4Polynomials | Documentation.SBV.Examples.Existentials.CRCPolynomial
findInjection | Documentation.SBV.Examples.Strings.SQLInjection
FiniteBits | Data.SBV.Trans, Data.SBV
finiteBitSize | Data.SBV.Trans, Data.SBV
first | Data.SBV.Either
firstQuery | Documentation.SBV.Examples.Queries.Concurrency
firstWeekend | Documentation.SBV.Examples.Optimization.Enumerate
Fish | Documentation.SBV.Examples.Puzzles.Fish
fishOwner | Documentation.SBV.Examples.Puzzles.Fish
Flag | Documentation.SBV.Examples.BitPrecise.Legato
FlagC | Documentation.SBV.Examples.BitPrecise.Legato
Flags | Documentation.SBV.Examples.BitPrecise.Legato
flags | Documentation.SBV.Examples.BitPrecise.Legato
FlagZ | Documentation.SBV.Examples.BitPrecise.Legato
flash | Documentation.SBV.Examples.Puzzles.U2Bridge
flIsCorrect | Documentation.SBV.Examples.BitPrecise.PrefixSum
floating | Data.SBV.RegExp
FloatingPoint | Data.SBV
floatToWord | Data.SBV.Internals
Flower | Documentation.SBV.Examples.Puzzles.Garden
flowerCount | Documentation.SBV.Examples.Puzzles.Garden
flyspeck | Documentation.SBV.Examples.DeltaSat.DeltaSat
foldl | Data.SBV.List
foldli | Data.SBV.List
foldr | Data.SBV.List
foldri | Data.SBV.List
Football | Documentation.SBV.Examples.Puzzles.Fish
Forall |
1 (Type/Class) | Data.SBV
2 (Data Constructor) | Data.SBV
ForallN |
1 (Type/Class) | Data.SBV
2 (Data Constructor) | Data.SBV
forceSVArg | Data.SBV.Internals
Forte | Data.SBV.Tools.GenTest
four | Documentation.SBV.Examples.Misc.Enumerate
fourCoat | Documentation.SBV.Examples.Lists.CountOutAndTransfer
FP |
1 (Type/Class) | Data.SBV.Float
2 (Data Constructor) | Data.SBV.Float
fp2fp | Data.SBV.Internals
fp54Bounds | Documentation.SBV.Examples.Misc.Floating
fpAbs | Data.SBV.Trans, Data.SBV
fpAdd | Data.SBV.Trans, Data.SBV
FPBFloat | Data.SBV
fpCompareObjectH | Data.SBV.Internals
fpDiv | Data.SBV.Trans, Data.SBV
FPDouble | Data.SBV
fpEncodeFloat | Data.SBV.Float
fpExponentSize | Data.SBV.Float
fpFMA | Data.SBV.Trans, Data.SBV
fpFromBigFloat | Data.SBV.Float
fpFromDouble | Data.SBV.Float
fpFromFloat | Data.SBV.Float
fpFromInteger | Data.SBV.Float
fpFromRational | Data.SBV.Float
fpFromRawRep | Data.SBV.Float
FPHalf | Data.SBV
fpInf | Data.SBV.Float
fpIsEqualObject | Data.SBV.Trans, Data.SBV
fpIsEqualObjectH | Data.SBV.Internals
fpIsInfinite | Data.SBV.Trans, Data.SBV
fpIsNaN | Data.SBV.Trans, Data.SBV
fpIsNegative | Data.SBV.Trans, Data.SBV
fpIsNegativeZero | Data.SBV.Trans, Data.SBV
fpIsNormal | Data.SBV.Trans, Data.SBV
fpIsNormalizedH | Data.SBV.Internals
fpIsPoint | Data.SBV.Trans, Data.SBV
fpIsPositive | Data.SBV.Trans, Data.SBV
fpIsPositiveZero | Data.SBV.Trans, Data.SBV
fpIsSubnormal | Data.SBV.Trans, Data.SBV
fpIsZero | Data.SBV.Trans, Data.SBV
fpMax | Data.SBV.Trans, Data.SBV
fpMaxH | Data.SBV.Internals
fpMin | Data.SBV.Trans, Data.SBV
fpMinH | Data.SBV.Internals
fpMul | Data.SBV.Trans, Data.SBV
fpNaN | Data.SBV.Float
fpNeg | Data.SBV.Trans, Data.SBV
FPOp | Data.SBV.Internals
FPQuad | Data.SBV
fpRem | Data.SBV.Trans, Data.SBV
fpRemH | Data.SBV.Internals
fpRoundToIntegral | Data.SBV.Trans, Data.SBV
fpRoundToIntegralH | Data.SBV.Internals
fpSignificandSize | Data.SBV.Float
FPSingle | Data.SBV
fpSqrt | Data.SBV.Trans, Data.SBV
fpSub | Data.SBV.Trans, Data.SBV
fpValue | Data.SBV.Float
fpZero | Data.SBV.Float
FP_Abs | Data.SBV.Internals
FP_Add | Data.SBV.Internals
FP_Cast | Data.SBV.Internals
FP_Div | Data.SBV.Internals
FP_FMA | Data.SBV.Internals
FP_IsInfinite | Data.SBV.Internals
FP_IsNaN | Data.SBV.Internals
FP_IsNegative | Data.SBV.Internals
FP_IsNormal | Data.SBV.Internals
FP_IsPositive | Data.SBV.Internals
FP_IsSubnormal | Data.SBV.Internals
FP_IsZero | Data.SBV.Internals
FP_Max | Data.SBV.Internals
FP_Min | Data.SBV.Internals
FP_Mul | Data.SBV.Internals
FP_Neg | Data.SBV.Internals
FP_ObjEqual | Data.SBV.Internals
FP_Reinterpret | Data.SBV.Internals
FP_Rem | Data.SBV.Internals
FP_RoundToIntegral | Data.SBV.Internals
FP_Sqrt | Data.SBV.Internals
FP_Sub | Data.SBV.Internals
Francine | Documentation.SBV.Examples.Puzzles.Orangutans
free |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
free_ |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
Fresh | Data.SBV.Control
fresh | Data.SBV.Control
freshArray |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
freshArray_ |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
freshLambdaArray | Data.SBV.Trans.Control
freshLambdaArray_ | Data.SBV.Trans.Control
freshVar |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
freshVar_ |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
Fri | Documentation.SBV.Examples.Optimization.Enumerate
Friday | Documentation.SBV.Examples.Queries.Enums
fromBitsBE | Data.SBV.Trans, Data.SBV
fromBitsLE | Data.SBV.Trans, Data.SBV
fromBool | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
fromBytes | Data.SBV
fromCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
fromJust | Data.SBV.Maybe
fromLeft | Data.SBV.Either
fromList | Data.SBV.Set
fromMaybe | Data.SBV.Maybe
fromMetricSpace | Data.SBV
fromNibbles | Documentation.SBV.Examples.Crypto.Prince
fromRight | Data.SBV.Either
fromSDouble | Data.SBV.Trans, Data.SBV
fromSFloat | Data.SBV.Trans, Data.SBV
fromSFloatingPoint | Data.SBV.Trans, Data.SBV
FromSized | Data.SBV.Trans, Data.SBV
fromSized | Data.SBV.Trans, Data.SBV
full | Data.SBV.Set
fullAdder | Data.SBV.Trans, Data.SBV
fullMultiplier | Data.SBV.Trans, Data.SBV