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 |
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 |
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 |
Football | Documentation.SBV.Examples.Puzzles.Fish |
forallDay | Documentation.SBV.Examples.Puzzles.Birthday |
forallMonth | Documentation.SBV.Examples.Puzzles.Birthday |
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 |
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 |
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.Trans, Data.SBV |
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 |