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

Index - A

A 
1 (Data Constructor)Documentation.SBV.Examples.Misc.Enumerate
2 (Type/Class)Documentation.SBV.Examples.WeakestPreconditions.Append
ABCData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
abcData.SBV.Trans, Data.SBV, Data.SBV.Dynamic
AbortData.SBV.Tools.WeakestPreconditions
AbortReachableData.SBV.Tools.WeakestPreconditions
AbsData.SBV.Internals
ActionsDocumentation.SBV.Examples.Puzzles.U2Bridge
AdamDocumentation.SBV.Examples.Puzzles.U2Bridge
adcDocumentation.SBV.Examples.BitPrecise.Legato
addDocumentation.SBV.Examples.Puzzles.AOC_2021_24
addAxiomData.SBV.Internals, Data.SBV.Trans, Data.SBV
AddExtCVData.SBV.Internals, Data.SBV.Trans, Data.SBV
addPolyData.SBV.Tools.Polynomial
addRoundKeyDocumentation.SBV.Examples.Crypto.AES
addSMTDefinitionData.SBV.Internals, Data.SBV
addSubDocumentation.SBV.Examples.CodeGeneration.AddSub
addSValOptGoalData.SBV.Internals
aes128IsCorrectDocumentation.SBV.Examples.Crypto.AES
aesDecryptDocumentation.SBV.Examples.Crypto.AES
aesEncryptDocumentation.SBV.Examples.Crypto.AES
aesInvRoundDocumentation.SBV.Examples.Crypto.AES
aesKeyScheduleDocumentation.SBV.Examples.Crypto.AES
aesLibComponentsDocumentation.SBV.Examples.Crypto.AES
aesRoundDocumentation.SBV.Examples.Crypto.AES
ageDocumentation.SBV.Examples.Puzzles.Murder
AlgIntervalData.SBV.Internals, Data.SBV
algorithm 
1 (Function)Documentation.SBV.Examples.WeakestPreconditions.Append
2 (Function)Documentation.SBV.Examples.WeakestPreconditions.Basics
3 (Function)Documentation.SBV.Examples.WeakestPreconditions.Fib
4 (Function)Documentation.SBV.Examples.WeakestPreconditions.GCD
5 (Function)Documentation.SBV.Examples.WeakestPreconditions.IntDiv
6 (Function)Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
7 (Function)Documentation.SBV.Examples.WeakestPreconditions.Length
8 (Function)Documentation.SBV.Examples.WeakestPreconditions.Sum
AlgPolyRootData.SBV.Internals, Data.SBV
AlgRationalData.SBV.Internals, Data.SBV
AlgRealData.SBV.Internals, Data.SBV.Trans, Data.SBV
AlgRealPoly 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
algRealToRationalData.SBV
ALLData.SBV.Internals, Data.SBV.Dynamic
AllData.SBV.RegExp, Data.SBV.Internals
AllCharData.SBV.RegExp, Data.SBV.Internals
allEqualData.SBV.Trans, Data.SBV
allModelsDocumentation.SBV.Examples.Misc.Auxiliary
Alloc 
1 (Type/Class)Documentation.SBV.Examples.Transformers.SymbolicEval
2 (Data Constructor)Documentation.SBV.Examples.Transformers.SymbolicEval
allocDocumentation.SBV.Examples.Transformers.SymbolicEval
allocateDocumentation.SBV.Examples.Optimization.VM
allocEnvDocumentation.SBV.Examples.Transformers.SymbolicEval
allowQuantifiedQueriesData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allPossibleTreesDocumentation.SBV.Examples.Queries.FourFours
allPuzzlesDocumentation.SBV.Examples.Puzzles.Sudoku
allSat 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
allSatHasPrefixExistentialsData.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatMaxModelCountData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatMaxModelCountReachedData.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatPrintAlongData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
AllSatResult 
1 (Type/Class)Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor)Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatResultsData.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatSolverReturnedDSatData.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatSolverReturnedUnknownData.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatWith 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
3 (Function)Data.SBV.Dynamic
AllStatisticsData.SBV.Trans.Control, Data.SBV.Control
almostWeekendDocumentation.SBV.Examples.Optimization.Enumerate
AloneDocumentation.SBV.Examples.Puzzles.Murder
ALUDocumentation.SBV.Examples.Puzzles.AOC_2021_24
And 
1 (Data Constructor)Data.SBV.Trans, Data.SBV
2 (Type/Class)Data.SBV.Trans, Data.SBV
3 (Data Constructor)Data.SBV.Internals
4 (Data Constructor)Documentation.SBV.Examples.Transformers.SymbolicEval
andDocumentation.SBV.Examples.Uninterpreted.Deduce
anyCharData.SBV.RegExp
AppC 
1 (Type/Class)Documentation.SBV.Examples.WeakestPreconditions.Append
2 (Data Constructor)Documentation.SBV.Examples.WeakestPreconditions.Append
approxRationalData.SBV.Trans, Data.SBV
AppS 
1 (Type/Class)Documentation.SBV.Examples.WeakestPreconditions.Append
2 (Data Constructor)Documentation.SBV.Examples.WeakestPreconditions.Append
ArithOverflowData.SBV.Tools.Overflow
ArrayContextData.SBV.Internals
ArrayFreeData.SBV.Internals
ArrayInfoData.SBV.Internals
ArrayMergeData.SBV.Internals
ArrayMutateData.SBV.Internals
ArrEqData.SBV.Internals
ArrReadData.SBV.Internals
asciiLetterData.SBV.RegExp
asciiLowerData.SBV.RegExp
asciiUpperData.SBV.RegExp
assertData.SBV.Tools.WeakestPreconditions
AssertionStackLevelsData.SBV.Trans.Control, Data.SBV.Control
AssertWithPenaltyData.SBV.Internals, Data.SBV.Trans, Data.SBV
assertWithPenalty 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
AssignData.SBV.Tools.WeakestPreconditions
assocPlusDocumentation.SBV.Examples.Misc.Floating
assocPlusRegularDocumentation.SBV.Examples.Misc.Floating
AUFLIAData.SBV.Trans, Data.SBV
AUFLIRAData.SBV.Trans, Data.SBV
AUFNIRAData.SBV.Trans, Data.SBV
augustDocumentation.SBV.Examples.Puzzles.Birthday
AuthorsData.SBV.Trans.Control, Data.SBV.Control
ax1Documentation.SBV.Examples.Uninterpreted.Deduce
ax2Documentation.SBV.Examples.Uninterpreted.Deduce
ax3Documentation.SBV.Examples.Uninterpreted.Deduce
axiomatizeFibDocumentation.SBV.Examples.WeakestPreconditions.Fib
axiomatizeGCDDocumentation.SBV.Examples.WeakestPreconditions.GCD