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

Index - I

IDocumentation.SBV.Examples.WeakestPreconditions.Basics
i 
1 (Function)Documentation.SBV.Examples.ProofTools.Fibonacci
2 (Function)Documentation.SBV.Examples.ProofTools.Sum
3 (Function)Documentation.SBV.Examples.WeakestPreconditions.Fib
4 (Function)Documentation.SBV.Examples.WeakestPreconditions.GCD
5 (Function)Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
6 (Function)Documentation.SBV.Examples.WeakestPreconditions.Sum
i2nDocumentation.SBV.Examples.TP.Peano
i2n2iDocumentation.SBV.Examples.TP.Peano
IAddDocumentation.SBV.Examples.TP.VM
IBindDocumentation.SBV.Examples.TP.VM
identifierData.SBV.RegExp
IdentityDocumentation.SBV.Examples.Puzzles.KnightsAndKnaves
IdleDocumentation.SBV.Examples.Lists.BoundedMutex
IDupDocumentation.SBV.Examples.TP.VM
idWFDocumentation.SBV.Examples.ADT.Types
IdxDocumentation.SBV.Examples.TP.BinarySearch
IEEEFloatConvertibleData.SBV.Trans, Data.SBV
IEEEFloatingData.SBV.Trans, Data.SBV
IEEEFPData.SBV.Internals
IfData.SBV.Tools.WeakestPreconditions
Iff 
1 (Type/Class)Data.SBV.Trans, Data.SBV
2 (Data Constructor)Data.SBV.Trans, Data.SBV
iffDocumentation.SBV.Examples.Puzzles.KnightsAndKnaves
IForgetDocumentation.SBV.Examples.TP.VM
ignoreExitCodeData.SBV.Trans.Control, Data.SBV.Control, Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
ImmDocumentation.SBV.Examples.Puzzles.AOC_2021_24
imperativeAppendDocumentation.SBV.Examples.WeakestPreconditions.Append
imperativeDivDocumentation.SBV.Examples.WeakestPreconditions.IntDiv
imperativeFibDocumentation.SBV.Examples.WeakestPreconditions.Fib
imperativeGCDDocumentation.SBV.Examples.WeakestPreconditions.GCD
imperativeIncDocumentation.SBV.Examples.WeakestPreconditions.Basics
imperativeLengthDocumentation.SBV.Examples.WeakestPreconditions.Length
imperativeSqrtDocumentation.SBV.Examples.WeakestPreconditions.IntSqrt
imperativeSumDocumentation.SBV.Examples.WeakestPreconditions.Sum
Implies 
1 (Data Constructor)Data.SBV.Internals
2 (Data Constructor)Documentation.SBV.Examples.Transformers.SymbolicEval
implodeData.SBV.List
IMulDocumentation.SBV.Examples.TP.VM
inArrayDocumentation.SBV.Examples.TP.BinarySearch
IncDocumentation.SBV.Examples.TP.VM
IncS 
1 (Type/Class)Documentation.SBV.Examples.WeakestPreconditions.Basics
2 (Data Constructor)Documentation.SBV.Examples.WeakestPreconditions.Basics
IndependentData.SBV.Internals, Data.SBV.Trans, Data.SBV
IndependentResultData.SBV.Trans, Data.SBV, Data.SBV.Dynamic
IndeterminateData.SBV.Tools.WeakestPreconditions
indexOfData.SBV.List
induct 
1 (Function)Data.SBV.Tools.Induction
2 (Function)Data.SBV.TP
InductionResultData.SBV.Tools.Induction
inductionSchemaData.SBV.Internals
InductionStepData.SBV.Tools.Induction
inductiveLemmaData.SBV.TP
inductiveLemmaWithData.SBV.TP
inductWith 
1 (Function)Data.SBV.Tools.Induction
2 (Function)Data.SBV.TP
InfiniteData.SBV.Internals, Data.SBV.Trans, Data.SBV
infinityData.SBV.Internals, Data.SBV.Trans, Data.SBV
InfoKeywordData.SBV.Trans.Control, Data.SBV.Control
inf_compl_le_botDocumentation.SBV.Examples.TP.ShefferStroke
inf_le_leftDocumentation.SBV.Examples.TP.ShefferStroke
inf_le_rightDocumentation.SBV.Examples.TP.ShefferStroke
InhabitantDocumentation.SBV.Examples.Puzzles.KnightsAndKnaves
initData.SBV.List
initCgStateData.SBV.Internals
InitialDocumentation.SBV.Examples.Puzzles.DieHard
InitiationData.SBV.Tools.Induction
initJugsDocumentation.SBV.Examples.Puzzles.Jugs
initMachineDocumentation.SBV.Examples.BitPrecise.Legato
initRC4Documentation.SBV.Examples.Crypto.RC4
initSDocumentation.SBV.Examples.Crypto.RC4
initsData.SBV.List
initsLengthData.SBV.TP.List
InitValsDocumentation.SBV.Examples.BitPrecise.Legato
inNewAssertionStack 
1 (Function)Data.SBV.Trans.Control
2 (Function)Data.SBV.Control
inpDocumentation.SBV.Examples.Puzzles.AOC_2021_24
inputsDocumentation.SBV.Examples.Puzzles.AOC_2021_24
inRangeData.SBV.Trans, Data.SBV
insert 
1 (Function)Data.SBV.Set
2 (Function)Documentation.SBV.Examples.TP.InsertionSort
insertionSortDocumentation.SBV.Examples.TP.InsertionSort
inSMTModeData.SBV.Internals
Inst 
1 (Type/Class)Data.SBV.TP
2 (Data Constructor)Data.SBV.TP
InstrDocumentation.SBV.Examples.TP.VM
InstructionDocumentation.SBV.Examples.BitPrecise.Legato
IntData.SBV.Trans, Data.SBV
Int16Data.SBV.Trans, Data.SBV
Int32Data.SBV.Trans, Data.SBV
Int64Data.SBV.Trans, Data.SBV
Int8Data.SBV.Trans, Data.SBV
InterData.SBV.RegExp, Data.SBV.Internals
interleaveData.SBV.TP.List
interleaveLenData.SBV.TP.List
interleaveRoundTripData.SBV.TP.List
internalAxiomData.SBV.Internals
internalConstraintData.SBV.Internals
internalVariableData.SBV.Internals
interpDocumentation.SBV.Examples.TP.VM
interpInEnvDocumentation.SBV.Examples.TP.VM
intersectionData.SBV.Set
intersectionsData.SBV.Set
IntervalData.SBV.Internals, Data.SBV.Trans, Data.SBV
intFuncAppStringDocumentation.SBV.Examples.ADT.Types
IntNData.SBV.Internals, Data.SBV.Trans, Data.SBV
intSizeOfData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
intToDigitData.SBV.Char
InvDocumentation.SBV.Examples.ProofTools.AddHorn
InvariantData.SBV.Tools.WeakestPreconditions
invariant 
1 (Function)Documentation.SBV.Examples.WeakestPreconditions.IntDiv
2 (Function)Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
3 (Function)Documentation.SBV.Examples.WeakestPreconditions.Length
InvariantMaintainData.SBV.Tools.WeakestPreconditions
InvariantPreData.SBV.Tools.WeakestPreconditions
invKeyExpansionDocumentation.SBV.Examples.Crypto.AES
invMixColumnsDocumentation.SBV.Examples.Crypto.AES
invRoundDocumentation.SBV.Examples.Crypto.Prince
io 
1 (Function)Data.SBV.Trans.Control
2 (Function)Data.SBV.Control
Ior 
1 (Type/Class)Data.SBV.Trans, Data.SBV
2 (Data Constructor)Data.SBV.Trans, Data.SBV
IPushNDocumentation.SBV.Examples.TP.VM
IPushVDocumentation.SBV.Examples.TP.VM
IRunData.SBV.Internals
isDocumentation.SBV.Examples.Puzzles.KnightsAndKnaves
isA 
1 (Function)Documentation.SBV.Examples.Misc.Enumerate
2 (Function)Documentation.SBV.Examples.Misc.FirstOrderLogic
isAdamDocumentation.SBV.Examples.Puzzles.U2Bridge
isAdd 
1 (Function)Documentation.SBV.Examples.ADT.Expr
2 (Function)Documentation.SBV.Examples.ADT.Param
isADTData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
ISafeData.SBV.Internals
isAloneDocumentation.SBV.Examples.Puzzles.Murder
isAlphaL1Data.SBV.Char
isAlphaNumL1Data.SBV.Char
isAmbalatDocumentation.SBV.Examples.Puzzles.Orangutans
isAppDocumentation.SBV.Examples.ADT.Types
isArrayData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isAsciiData.SBV.Char
isAsciiLowerData.SBV.Char
isAsciiUpperData.SBV.Char
isAugDocumentation.SBV.Examples.Puzzles.Birthday
isB 
1 (Function)Documentation.SBV.Examples.Misc.Enumerate
2 (Function)Documentation.SBV.Examples.Misc.FirstOrderLogic
isBarDocumentation.SBV.Examples.Puzzles.Murder
isBasahanDocumentation.SBV.Examples.Puzzles.Orangutans
isBaseballDocumentation.SBV.Examples.Puzzles.Fish
isBeachDocumentation.SBV.Examples.Puzzles.Murder
isBeerDocumentation.SBV.Examples.Puzzles.Fish
isBigToSmallDocumentation.SBV.Examples.Puzzles.DieHard
isBirdDocumentation.SBV.Examples.Puzzles.Fish
isBlackDocumentation.SBV.Examples.Puzzles.HexPuzzle
isBlue 
1 (Function)Documentation.SBV.Examples.Puzzles.Fish
2 (Function)Documentation.SBV.Examples.Puzzles.Garden
3 (Function)Documentation.SBV.Examples.Puzzles.HexPuzzle
isBonoDocumentation.SBV.Examples.Puzzles.U2Bridge
isBooleanData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isBoundedData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isBritonDocumentation.SBV.Examples.Puzzles.Fish
isBystanderDocumentation.SBV.Examples.Puzzles.Murder
isC 
1 (Function)Documentation.SBV.Examples.Misc.Enumerate
2 (Function)Documentation.SBV.Examples.Misc.FirstOrderLogic
isCatDocumentation.SBV.Examples.Puzzles.Fish
isCgDriverData.SBV.Internals
isCgMakefileData.SBV.Internals
isCharData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isCodeGenModeData.SBV.Internals
isCoffeeDocumentation.SBV.Examples.Puzzles.Fish
isConcreteData.SBV.Internals, Data.SBV.Trans, Data.SBV
isConcretelyData.SBV.Internals, Data.SBV.Trans, Data.SBV
isControlL1Data.SBV.Char
isCriticalDocumentation.SBV.Examples.Lists.BoundedMutex
isD14Documentation.SBV.Examples.Puzzles.Birthday
isD15Documentation.SBV.Examples.Puzzles.Birthday
isD16Documentation.SBV.Examples.Puzzles.Birthday
isD17Documentation.SBV.Examples.Puzzles.Birthday
isD18Documentation.SBV.Examples.Puzzles.Birthday
isD19Documentation.SBV.Examples.Puzzles.Birthday
isDaneDocumentation.SBV.Examples.Puzzles.Fish
isDigitData.SBV.Char
isDivideDocumentation.SBV.Examples.Queries.FourFours
isDogDocumentation.SBV.Examples.Puzzles.Fish
isDollyDocumentation.SBV.Examples.Puzzles.Orangutans
isDoubleData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isEdgeDocumentation.SBV.Examples.Puzzles.U2Bridge
isEmptyData.SBV.Set
isEmptyBigDocumentation.SBV.Examples.Puzzles.DieHard
isEmptySmallDocumentation.SBV.Examples.Puzzles.DieHard
ISetupData.SBV.Internals
isEvaDocumentation.SBV.Examples.Puzzles.Orangutans
isEven 
1 (Function)Documentation.SBV.Examples.Misc.Definitions
2 (Function)Documentation.SBV.Examples.TP.GCD
isEvenOddDocumentation.SBV.Examples.Misc.Definitions
isExptDocumentation.SBV.Examples.Queries.FourFours
isFactorialDocumentation.SBV.Examples.Queries.FourFours
isFalsityDocumentation.SBV.Examples.Puzzles.KnightsAndKnaves
isFemaleDocumentation.SBV.Examples.Puzzles.Murder
isFillBigDocumentation.SBV.Examples.Puzzles.DieHard
isFillSmallDocumentation.SBV.Examples.Puzzles.DieHard
isFishDocumentation.SBV.Examples.Puzzles.Fish
isFloatData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isFootballDocumentation.SBV.Examples.Puzzles.Fish
isFPData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isFrancineDocumentation.SBV.Examples.Puzzles.Orangutans
isFriDocumentation.SBV.Examples.Optimization.Enumerate
isFridayDocumentation.SBV.Examples.Queries.Enums
isFullData.SBV.Set
isGermanDocumentation.SBV.Examples.Puzzles.Fish
isGracieDocumentation.SBV.Examples.Puzzles.Orangutans
isGreen 
1 (Function)Documentation.SBV.Examples.Puzzles.Fish
2 (Function)Documentation.SBV.Examples.Puzzles.HexPuzzle
isHereDocumentation.SBV.Examples.Puzzles.U2Bridge
isHexDigitData.SBV.Char
isHockeyDocumentation.SBV.Examples.Puzzles.Fish
isHorseDocumentation.SBV.Examples.Puzzles.Fish
isIdDocumentation.SBV.Examples.ADT.Param
isIdleDocumentation.SBV.Examples.Lists.BoundedMutex
isInfixOfData.SBV.List
isInitialDocumentation.SBV.Examples.Puzzles.DieHard
isJulDocumentation.SBV.Examples.Puzzles.Birthday
isJunDocumentation.SBV.Examples.Puzzles.Birthday
isJustData.SBV.Maybe
isKendisiDocumentation.SBV.Examples.Puzzles.Orangutans
isKillerDocumentation.SBV.Examples.Puzzles.Murder
isKnaveDocumentation.SBV.Examples.Puzzles.KnightsAndKnaves
isKnightDocumentation.SBV.Examples.Puzzles.KnightsAndKnaves
isLamDocumentation.SBV.Examples.ADT.Types
isLarryDocumentation.SBV.Examples.Puzzles.U2Bridge
isLatin1Data.SBV.Char
isLeftData.SBV.Either
isLet 
1 (Function)Documentation.SBV.Examples.ADT.Expr
2 (Function)Documentation.SBV.Examples.ADT.Param
isLetterL1Data.SBV.Char
isLinearOrderData.SBV
isListData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isLowerL1Data.SBV.Char
isMagicDocumentation.SBV.Examples.Puzzles.MagicSquare
isMaleDocumentation.SBV.Examples.Puzzles.Murder
isMarkL1Data.SBV.Char
isMayDocumentation.SBV.Examples.Puzzles.Birthday
isMerahDocumentation.SBV.Examples.Puzzles.Orangutans
isMilkDocumentation.SBV.Examples.Puzzles.Fish
isMinusDocumentation.SBV.Examples.Queries.FourFours
isMonDocumentation.SBV.Examples.Optimization.Enumerate
isMondayDocumentation.SBV.Examples.Queries.Enums
isMul 
1 (Function)Documentation.SBV.Examples.ADT.Expr
2 (Function)Documentation.SBV.Examples.ADT.Param
isNegateDocumentation.SBV.Examples.Queries.FourFours
isNonModelVarData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isNorwegianDocumentation.SBV.Examples.Puzzles.Fish
isNothingData.SBV.Maybe
isNumberL1Data.SBV.Char
isOctDigitData.SBV.Char
isOdd 
1 (Function)Documentation.SBV.Examples.Misc.Definitions
2 (Function)Documentation.SBV.Examples.TP.GCD
isOfalloDocumentation.SBV.Examples.Puzzles.Orangutans
isPartialOrderData.SBV
isPermutation 
1 (Function)Documentation.SBV.Examples.TP.SortHelpers
2 (Function)Documentation.SBV.Examples.TP.InsertionSort
isPermutationOfDocumentation.SBV.Examples.BitPrecise.MergeSort
isPiecewiseLinearOrderData.SBV
isPlusDocumentation.SBV.Examples.Queries.FourFours
isPrefixOfData.SBV.List
isPrintL1Data.SBV.Char
isProperSubsetOfData.SBV.Set
isPunctuationL1Data.SBV.Char
isQuirrelDocumentation.SBV.Examples.Puzzles.Orangutans
isRationalData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isReadyDocumentation.SBV.Examples.Lists.BoundedMutex
isRealData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isRed 
1 (Function)Documentation.SBV.Examples.Puzzles.Fish
2 (Function)Documentation.SBV.Examples.Puzzles.Garden
3 (Function)Documentation.SBV.Examples.Puzzles.HexPuzzle
isRegularCVData.SBV.Internals
isReservedData.SBV.Internals
isRightData.SBV.Either
isRoundingModeData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isSafeData.SBV.Trans, Data.SBV
isSatDocumentation.SBV.Examples.Optimization.Enumerate
isSatisfiable 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
isSatisfiableWith 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
isSaturdayDocumentation.SBV.Examples.Queries.Enums
isSeparatorL1Data.SBV.Char
isSetData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isShamirDocumentation.SBV.Examples.Puzzles.Orangutans
isSignedData.SBV.Trans, Data.SBV
isSmallToBigDocumentation.SBV.Examples.Puzzles.DieHard
isSpaceL1Data.SBV.Char
isSqrtDocumentation.SBV.Examples.Queries.FourFours
isStringData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isSubsetOfData.SBV.Set
isSuccDocumentation.SBV.Examples.TP.Peano
isSuffixOfData.SBV.List
isSunDocumentation.SBV.Examples.Optimization.Enumerate
isSundayDocumentation.SBV.Examples.Queries.Enums
isSwedeDocumentation.SBV.Examples.Puzzles.Fish
isSymbolicData.SBV.Internals, Data.SBV.Trans, Data.SBV
isSymbolL1Data.SBV.Char
IStageData.SBV.Internals
isTarakanDocumentation.SBV.Examples.Puzzles.Orangutans
isTArrDocumentation.SBV.Examples.ADT.Types
isTeaDocumentation.SBV.Examples.Puzzles.Fish
isTennisDocumentation.SBV.Examples.Puzzles.Fish
isTheorem 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
isTheoremWith 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
isThereDocumentation.SBV.Examples.Puzzles.U2Bridge
isThuDocumentation.SBV.Examples.Optimization.Enumerate
isThursdayDocumentation.SBV.Examples.Queries.Enums
isTimesDocumentation.SBV.Examples.Queries.FourFours
isTIntDocumentation.SBV.Examples.ADT.Types
isTreeOrderData.SBV
isTruthDocumentation.SBV.Examples.Puzzles.KnightsAndKnaves
isTStrDocumentation.SBV.Examples.ADT.Types
isTueDocumentation.SBV.Examples.Optimization.Enumerate
isTuesdayDocumentation.SBV.Examples.Queries.Enums
isTupleData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isUnboundedData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isUninterpretedData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isUniversalData.SBV.Set
isUpperL1Data.SBV.Char
isVacuousProof 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
isVacuousProofWith 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
isVal 
1 (Function)Documentation.SBV.Examples.ADT.Expr
2 (Function)Documentation.SBV.Examples.ADT.Param
isValid 
1 (Function)Documentation.SBV.Examples.ADT.Expr
2 (Function)Documentation.SBV.Examples.ADT.Param
3 (Function)Documentation.SBV.Examples.Puzzles.NQueens
4 (Function)Documentation.SBV.Examples.Puzzles.U2Bridge
isVar 
1 (Function)Documentation.SBV.Examples.ADT.Expr
2 (Function)Documentation.SBV.Examples.ADT.Param
3 (Function)Documentation.SBV.Examples.ADT.Types
isVictimDocumentation.SBV.Examples.Puzzles.Murder
isVolleyballDocumentation.SBV.Examples.Puzzles.Fish
isWaterDocumentation.SBV.Examples.Puzzles.Fish
isWedDocumentation.SBV.Examples.Optimization.Enumerate
isWednesdayDocumentation.SBV.Examples.Queries.Enums
isWeekendDocumentation.SBV.Examples.Optimization.Enumerate
isWhiteDocumentation.SBV.Examples.Puzzles.Fish
isYellow 
1 (Function)Documentation.SBV.Examples.Puzzles.Fish
2 (Function)Documentation.SBV.Examples.Puzzles.Garden
isZeroDocumentation.SBV.Examples.TP.Peano
IteData.SBV.Internals
iteData.SBV.Trans, Data.SBV
iteLazyData.SBV.Trans, Data.SBV
itesData.SBV.Tools.Polynomial