| C | |
| 1 (Data Constructor) | Data.SBV.Tools.GenTest |
| 2 (Data Constructor) | Documentation.SBV.Examples.Misc.Enumerate |
| c1 | Documentation.SBV.Examples.Puzzles.Coins |
| c2 | Documentation.SBV.Examples.Puzzles.Coins |
| c3 | Documentation.SBV.Examples.Puzzles.Coins |
| c4 | Documentation.SBV.Examples.Puzzles.Coins |
| c5 | Documentation.SBV.Examples.Puzzles.Coins |
| c6 | Documentation.SBV.Examples.Puzzles.Coins |
| cache | Data.SBV.Internals |
| Cached | Data.SBV.Internals |
| CAlgReal | Data.SBV.Internals, Data.SBV.Dynamic |
| capabilities | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| capacity | Documentation.SBV.Examples.Puzzles.Jugs |
| caseSplit | |
| 1 (Function) | Data.SBV.Trans.Control |
| 2 (Function) | Data.SBV.Control |
| Cat | Documentation.SBV.Examples.Puzzles.Fish |
| CChar | Data.SBV.Internals, Data.SBV.Dynamic |
| CDouble | Data.SBV.Internals, Data.SBV.Dynamic |
| ceilingHighEnoughForHuman | Documentation.SBV.Examples.Misc.Newtypes |
| CEither | Data.SBV.Internals, Data.SBV.Dynamic |
| CFloat | Data.SBV.Internals, Data.SBV.Dynamic |
| CFP | Data.SBV.Internals, Data.SBV.Dynamic |
| cg1 | Documentation.SBV.Examples.CodeGeneration.CRC_USB5 |
| cg2 | Documentation.SBV.Examples.CodeGeneration.CRC_USB5 |
| cgAddDecl | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgAddLDFlags | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgAddPrototype | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgAES128BlockEncrypt | Documentation.SBV.Examples.Crypto.AES |
| cgAES128Library | Documentation.SBV.Examples.Crypto.AES |
| cgAESLibrary | Documentation.SBV.Examples.Crypto.AES |
| CgArray | Data.SBV.Internals |
| CgAtomic | Data.SBV.Internals |
| CgConfig | |
| 1 (Type/Class) | Data.SBV.Internals |
| 2 (Data Constructor) | Data.SBV.Internals |
| cgDecls | Data.SBV.Internals |
| CgDouble | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| CgDriver | Data.SBV.Internals |
| cgDriverVals | Data.SBV.Internals |
| cgFinalConfig | Data.SBV.Internals |
| CgFloat | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgGenDriver | Data.SBV.Internals |
| cgGenerateDriver | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgGenerateMakefile | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgGenMakefile | Data.SBV.Internals |
| CgHeader | Data.SBV.Internals |
| cgIgnoreAsserts | Data.SBV.Internals |
| cgIgnoreSAssert | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgInput | Data.SBV.Tools.CodeGen, Data.SBV.Internals |
| cgInputArr | Data.SBV.Tools.CodeGen, Data.SBV.Internals |
| cgInputs | Data.SBV.Internals |
| cgInteger | Data.SBV.Internals |
| cgIntegerSize | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgLDFlags | Data.SBV.Internals |
| CgLongDouble | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| CgMakefile | Data.SBV.Internals |
| cgOutput | Data.SBV.Tools.CodeGen, Data.SBV.Internals |
| cgOutputArr | Data.SBV.Tools.CodeGen, Data.SBV.Internals |
| cgOutputs | Data.SBV.Internals |
| cgOverwriteFiles | Data.SBV.Tools.CodeGen, Data.SBV.Internals |
| cgOverwriteGenerated | Data.SBV.Internals |
| cgPerformRTCs | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| CgPgmBundle | |
| 1 (Type/Class) | Data.SBV.Internals |
| 2 (Data Constructor) | Data.SBV.Internals |
| CgPgmKind | Data.SBV.Internals |
| cgPrototypes | Data.SBV.Internals |
| cgReal | Data.SBV.Internals |
| cgReturn | Data.SBV.Tools.CodeGen, Data.SBV.Internals |
| cgReturnArr | Data.SBV.Tools.CodeGen, Data.SBV.Internals |
| cgReturns | Data.SBV.Internals |
| cgRTC | Data.SBV.Internals |
| cgSetDriverValues | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgSHA256 | Documentation.SBV.Examples.Crypto.SHA |
| cgShowU8InHex | Data.SBV.Internals |
| cgShowU8UsingHex | Data.SBV.Tools.CodeGen, Data.SBV.Internals |
| CgSource | Data.SBV.Internals |
| CgSRealType | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| cgSRealType | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic |
| CgState | |
| 1 (Type/Class) | Data.SBV.Internals |
| 2 (Data Constructor) | Data.SBV.Internals |
| cgSym | Data.SBV.Tools.CodeGen, Data.SBV.Internals |
| CgTarget | Data.SBV.Internals |
| cgUninterpret | Data.SBV.Trans, Data.SBV |
| CgVal | Data.SBV.Internals |
| ch | Documentation.SBV.Examples.Crypto.SHA |
| check | |
| 1 (Function) | Documentation.SBV.Examples.Puzzles.MagicSquare |
| 2 (Function) | Documentation.SBV.Examples.Puzzles.Sudoku |
| 3 (Function) | Documentation.SBV.Examples.Transformers.SymbolicEval |
| checkArithOverflow | Documentation.SBV.Examples.BitPrecise.BrokenSearch |
| checkCorrectMidValue | Documentation.SBV.Examples.BitPrecise.BrokenSearch |
| CheckedArithmetic | Data.SBV.Tools.Overflow |
| checkedDiv | Documentation.SBV.Examples.Misc.NoDiv0 |
| checkMutex | Documentation.SBV.Examples.Lists.BoundedMutex |
| checkOverflow | Documentation.SBV.Examples.BitPrecise.Legato |
| checkOverflowCorrect | Documentation.SBV.Examples.BitPrecise.Legato |
| CheckResult | Documentation.SBV.Examples.Transformers.SymbolicEval |
| checkSat | |
| 1 (Function) | Data.SBV.Trans.Control |
| 2 (Function) | Data.SBV.Control |
| checkSatAssuming | |
| 1 (Function) | Data.SBV.Trans.Control |
| 2 (Function) | Data.SBV.Control |
| checkSatAssumingWithUnsatisfiableSet | |
| 1 (Function) | Data.SBV.Trans.Control |
| 2 (Function) | Data.SBV.Control |
| CheckSatResult | Data.SBV.Trans.Control, Data.SBV.Control |
| checkSatUsing | |
| 1 (Function) | Data.SBV.Trans.Control |
| 2 (Function) | Data.SBV.Control |
| cheryl | Documentation.SBV.Examples.Puzzles.Birthday |
| chex | Data.SBV.Internals |
| chr | Data.SBV.Char |
| chunk | Documentation.SBV.Examples.Puzzles.MagicSquare |
| chunkBy | Documentation.SBV.Examples.Crypto.SHA |
| CInteger | Data.SBV.Internals, Data.SBV.Dynamic |
| classify | Documentation.SBV.Examples.Uninterpreted.UISortAllSat |
| clc | Documentation.SBV.Examples.BitPrecise.Legato |
| clearBit | Data.SBV.Trans, Data.SBV |
| CList | Data.SBV.Internals, Data.SBV.Dynamic |
| Closed | Data.SBV.Tools.Range |
| ClosedPoint | Data.SBV |
| CMaybe | Data.SBV.Internals, Data.SBV.Dynamic |
| coat | Documentation.SBV.Examples.Lists.CountOutAndTransfer |
| coatCheck | Documentation.SBV.Examples.Lists.CountOutAndTransfer |
| CodeGen | Data.SBV.Internals |
| codeGen | |
| 1 (Function) | Data.SBV.Internals |
| 2 (Function) | Documentation.SBV.Examples.BitPrecise.MergeSort |
| Coffee | Documentation.SBV.Examples.Puzzles.Fish |
| Coin | Documentation.SBV.Examples.Puzzles.Coins |
| col | Documentation.SBV.Examples.Puzzles.Garden |
| Color | |
| 1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Fish |
| 2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Garden |
| 3 (Type/Class) | Documentation.SBV.Examples.Puzzles.HexPuzzle |
| combinations | Documentation.SBV.Examples.Puzzles.Coins |
| Comp | Data.SBV.RegExp, Data.SBV.Internals |
| compileToC | Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
| compileToC' | Data.SBV.Internals |
| compileToCLib | Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
| compileToCLib' | Data.SBV.Internals |
| complement | |
| 1 (Function) | Data.SBV.Trans, Data.SBV |
| 2 (Function) | Data.SBV.Set |
| complementBit | Data.SBV.Trans, Data.SBV |
| ComplementSet | Data.SBV.Internals, Data.SBV |
| Conc | Data.SBV.RegExp, Data.SBV.Internals |
| Concat | Documentation.SBV.Examples.Strings.SQLInjection |
| concat | |
| 1 (Function) | Data.SBV.String |
| 2 (Function) | Data.SBV.List |
| Concrete | Data.SBV.Internals |
| conditionalSetClearCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks |
| Consecution | Data.SBV.Tools.Induction |
| Const | |
| 1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Murder |
| 2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Murder |
| 3 (Data Constructor) | Documentation.SBV.Examples.Strings.SQLInjection |
| constrain | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| constrainWithAttribute | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| content | Documentation.SBV.Examples.Puzzles.Jugs |
| contextState | Data.SBV.Internals |
| correctness | |
| 1 (Function) | Documentation.SBV.Examples.BitPrecise.MergeSort |
| 2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Append |
| 3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics |
| 4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib |
| 5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD |
| 6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv |
| 7 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt |
| 8 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length |
| 9 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum |
| correctnessTheorem | Documentation.SBV.Examples.BitPrecise.Legato |
| Count | Documentation.SBV.Examples.Puzzles.Counts |
| count | |
| 1 (Function) | Documentation.SBV.Examples.Puzzles.Counts |
| 2 (Function) | Documentation.SBV.Examples.Puzzles.Garden |
| Counterexample | Documentation.SBV.Examples.Transformers.SymbolicEval |
| countLeadingZeros | Data.SBV.Trans, Data.SBV |
| counts | Documentation.SBV.Examples.Puzzles.Counts |
| countTrailingZeros | Data.SBV.Trans, Data.SBV |
| crack | Data.SBV |
| crackNum | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| CRational | Data.SBV.Internals, Data.SBV.Dynamic |
| crc | Data.SBV.Tools.Polynomial |
| crcBV | Data.SBV.Tools.Polynomial |
| crcGood | |
| 1 (Function) | Documentation.SBV.Examples.CodeGeneration.CRC_USB5 |
| 2 (Function) | Documentation.SBV.Examples.Existentials.CRCPolynomial |
| crcUSB | Documentation.SBV.Examples.CodeGeneration.CRC_USB5 |
| crcUSB' | Documentation.SBV.Examples.CodeGeneration.CRC_USB5 |
| crc_48_16 | Documentation.SBV.Examples.Existentials.CRCPolynomial |
| create | Data.SBV.Control |
| Critical | Documentation.SBV.Examples.Lists.BoundedMutex |
| crossTime | Documentation.SBV.Examples.Puzzles.U2Bridge |
| csDemo1 | Documentation.SBV.Examples.Queries.CaseSplit |
| csDemo2 | Documentation.SBV.Examples.Queries.CaseSplit |
| CSet | Data.SBV.Internals, Data.SBV.Dynamic |
| CString | Data.SBV.Internals, Data.SBV.Dynamic |
| CTuple | Data.SBV.Internals, Data.SBV.Dynamic |
| CUserSort | Data.SBV.Internals, Data.SBV.Dynamic |
| CustomLogic | Data.SBV.Trans, Data.SBV |
| CV | |
| 1 (Type/Class) | Data.SBV.Internals, Data.SBV.Dynamic |
| 2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Dynamic |
| CVal | Data.SBV.Internals, Data.SBV.Dynamic |
| CVC4 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| cvc4 | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| CVC5 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| cvc5 | Data.SBV |
| cvSameType | Data.SBV.Internals |
| cvtModel | Data.SBV.Trans, Data.SBV |
| cvToBool | Data.SBV.Internals, Data.SBV.Dynamic |
| cvToSMTLib | Data.SBV.Internals |
| cvVal | Data.SBV.Internals, Data.SBV.Dynamic |