| 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 |
| forAll | |
| 1 (Function) | Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| forall | |
| 1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| forallDay | Documentation.SBV.Examples.Puzzles.Birthday |
| forallMonth | Documentation.SBV.Examples.Puzzles.Birthday |
| forAll_ | |
| 1 (Function) | Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| forall_ | |
| 1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| forceSVArg | Data.SBV.Internals |
| forSome | |
| 1 (Function) | Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| forSome_ | |
| 1 (Function) | Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| Forte | Data.SBV.Tools.GenTest |
| four | Documentation.SBV.Examples.Misc.Enumerate |
| 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 |
| 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 |
| 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 |