| S |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.Crypto.RC4 | 
| 2 (Type/Class) | Documentation.SBV.Examples.ProofTools.BMC | 
| 3 (Data Constructor) | Documentation.SBV.Examples.ProofTools.BMC | 
| 4 (Type/Class) | Documentation.SBV.Examples.ProofTools.Fibonacci | 
| 5 (Data Constructor) | Documentation.SBV.Examples.ProofTools.Fibonacci | 
| 6 (Type/Class) | Documentation.SBV.Examples.ProofTools.Strengthen | 
| 7 (Data Constructor) | Documentation.SBV.Examples.ProofTools.Strengthen | 
| 8 (Type/Class) | Documentation.SBV.Examples.ProofTools.Sum | 
| 9 (Data Constructor) | Documentation.SBV.Examples.ProofTools.Sum | 
| 10 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt | 
| 11 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Length | 
| 12 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Sum | 
| s |  | 
| 1 (Function) | Documentation.SBV.Examples.ProofTools.Sum | 
| 2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum | 
| sA | Documentation.SBV.Examples.Misc.Enumerate | 
| sAdam | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| safe |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| SafeResult |  | 
| 1 (Type/Class) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| 2 (Data Constructor) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| safeWith |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| 3 (Function) | Data.SBV.Dynamic | 
| sailors | Documentation.SBV.Examples.Existentials.Diophantine | 
| sAll | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sAlone | Documentation.SBV.Examples.Puzzles.Murder | 
| sAnd | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sAny | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| SArr | Data.SBV.Dynamic | 
| SArray |  | 
| 1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| sAssert | Data.SBV.Trans, Data.SBV | 
| Sat |  | 
| 1 (Data Constructor) | Data.SBV.Trans.Control, Data.SBV.Control | 
| 2 (Data Constructor) | Documentation.SBV.Examples.Optimization.Enumerate | 
| sat |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| satCmd | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| satConcurrentWithAll |  | 
| 1 (Function) | Data.SBV.Trans, Data.SBV | 
| 2 (Function) | Data.SBV.Dynamic | 
| satConcurrentWithAny |  | 
| 1 (Function) | Data.SBV.Trans, Data.SBV | 
| 2 (Function) | Data.SBV.Dynamic | 
| SatExtField | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| Satisfiable | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| SatModel | Data.SBV.Trans, Data.SBV | 
| SatResult |  | 
| 1 (Type/Class) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| 2 (Data Constructor) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| satTrackUFs | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| Saturday | Documentation.SBV.Examples.Queries.Enums | 
| satWith |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| 3 (Function) | Data.SBV.Dynamic | 
| satWithAll |  | 
| 1 (Function) | Data.SBV.Trans, Data.SBV | 
| 2 (Function) | Data.SBV.Dynamic | 
| satWithAny |  | 
| 1 (Function) | Data.SBV.Trans, Data.SBV | 
| 2 (Function) | Data.SBV.Dynamic | 
| SaveTiming | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| SB | Documentation.SBV.Examples.Uninterpreted.Deduce | 
| sB | Documentation.SBV.Examples.Misc.Enumerate | 
| sBar | Documentation.SBV.Examples.Puzzles.Murder | 
| sBarrelRotateLeft | Data.SBV.Trans, Data.SBV | 
| sBarrelRotateRight | Data.SBV.Trans, Data.SBV | 
| sBaseball | Documentation.SBV.Examples.Puzzles.Fish | 
| sBeach | Documentation.SBV.Examples.Puzzles.Murder | 
| sBeer | Documentation.SBV.Examples.Puzzles.Fish | 
| SBeverage | Documentation.SBV.Examples.Puzzles.Fish | 
| sbin | Data.SBV.Internals | 
| sbinI | Data.SBV.Internals | 
| SBinOp | Documentation.SBV.Examples.Queries.FourFours | 
| sBird | Documentation.SBV.Examples.Puzzles.Fish | 
| sBlack | Documentation.SBV.Examples.Puzzles.HexPuzzle | 
| sBlue |  | 
| 1 (Function) | Documentation.SBV.Examples.Puzzles.Fish | 
| 2 (Function) | Documentation.SBV.Examples.Puzzles.Garden | 
| 3 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle | 
| sBono | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| SBool | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sBool |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sBools |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sBool_ | Data.SBV | 
| sbox | Documentation.SBV.Examples.Crypto.AES | 
| sboxInverseCorrect | Documentation.SBV.Examples.Crypto.AES | 
| sboxTable | Documentation.SBV.Examples.Crypto.AES | 
| sBriton | Documentation.SBV.Examples.Puzzles.Fish | 
| SButton | Documentation.SBV.Examples.Puzzles.HexPuzzle | 
| SBV |  | 
| 1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| SBVApp | Data.SBV.Internals | 
| sbvCheckSolverInstallation | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| SBVCodeGen |  | 
| 1 (Type/Class) | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| SBVException |  | 
| 1 (Type/Class) | Data.SBV.Trans, Data.SBV | 
| 2 (Data Constructor) | Data.SBV.Trans, Data.SBV | 
| sbvExceptionConfig | Data.SBV.Trans, Data.SBV | 
| sbvExceptionDescription | Data.SBV.Trans, Data.SBV | 
| sbvExceptionExitCode | Data.SBV.Trans, Data.SBV | 
| sbvExceptionExpected | Data.SBV.Trans, Data.SBV | 
| sbvExceptionHint | Data.SBV.Trans, Data.SBV | 
| sbvExceptionReason | Data.SBV.Trans, Data.SBV | 
| sbvExceptionReceived | Data.SBV.Trans, Data.SBV | 
| sbvExceptionSent | Data.SBV.Trans, Data.SBV | 
| sbvExceptionStdErr | Data.SBV.Trans, Data.SBV | 
| sbvExceptionStdOut | Data.SBV.Trans, Data.SBV | 
| SBVExpr | Data.SBV.Internals | 
| SBVPgm |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| sbvQuickCheck | Data.SBV.Trans, Data.SBV | 
| SBVRunMode | Data.SBV.Internals | 
| sbvToSV | Data.SBV.Internals | 
| sbvToSymSV | Data.SBV.Internals | 
| SBVType |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| sbvUninterpret | Data.SBV.Trans, Data.SBV | 
| sBystander | Documentation.SBV.Examples.Puzzles.Murder | 
| sC | Documentation.SBV.Examples.Misc.Enumerate | 
| sCase | Documentation.SBV.Examples.Queries.FourFours | 
| sCat | Documentation.SBV.Examples.Puzzles.Fish | 
| SChar | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sChar |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sChars |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sChar_ | Data.SBV | 
| sCoffee | Documentation.SBV.Examples.Puzzles.Fish | 
| SColor |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Fish | 
| 2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Garden | 
| 3 (Type/Class) | Documentation.SBV.Examples.Puzzles.HexPuzzle | 
| sComparableSWord32AsSFloat | Data.SBV.Internals | 
| sComparableSWord64AsSDouble | Data.SBV.Internals | 
| sComparableSWordAsSFloatingPoint | Data.SBV.Internals | 
| sCountLeadingZeros | Data.SBV.Trans, Data.SBV | 
| sCountTrailingZeros | Data.SBV.Trans, Data.SBV | 
| scriptBody | Data.SBV.Internals | 
| scriptModel | Data.SBV.Internals | 
| sCritical | Documentation.SBV.Examples.Lists.BoundedMutex | 
| sCrossTime | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| sDane | Documentation.SBV.Examples.Puzzles.Fish | 
| SDay |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.Optimization.Enumerate | 
| 2 (Type/Class) | Documentation.SBV.Examples.Queries.Enums | 
| sDiv | Data.SBV.Trans, Data.SBV | 
| sDivide | Documentation.SBV.Examples.Queries.FourFours | 
| SDivisible | Data.SBV.Trans, Data.SBV | 
| sDivMod | Data.SBV.Trans, Data.SBV | 
| sDog | Documentation.SBV.Examples.Puzzles.Fish | 
| SDouble | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sDouble |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sDoubleAsComparableSWord64 | Data.SBV.Internals | 
| sDoubleAsSWord64 | Data.SBV.Trans, Data.SBV | 
| sDoubles |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sDouble_ | Data.SBV | 
| SE | Documentation.SBV.Examples.Misc.Enumerate | 
| search | Documentation.SBV.Examples.Puzzles.HexPuzzle | 
| second | Data.SBV.Either | 
| secondQuery | Documentation.SBV.Examples.Queries.Concurrency | 
| sEdge | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| SEither | Data.SBV.Internals, Data.SBV | 
| sEither | Data.SBV | 
| sEithers | Data.SBV | 
| sEither_ | Data.SBV | 
| select | Data.SBV.Trans, Data.SBV | 
| selectRe | Documentation.SBV.Examples.Strings.SQLInjection | 
| sElem | Data.SBV.Trans, Data.SBV | 
| sendMoreMoney | Documentation.SBV.Examples.Puzzles.SendMoreMoney | 
| sendRequestToSolver | Data.SBV.Internals | 
| sendStringToSolver | Data.SBV.Internals | 
| Seq | Data.SBV.Tools.WeakestPreconditions | 
| SeqConcat | Data.SBV.Internals | 
| SeqContains | Data.SBV.Internals | 
| SeqIndexOf | Data.SBV.Internals | 
| SeqLen | Data.SBV.Internals | 
| SeqNth | Data.SBV.Internals | 
| SeqOp |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| SeqPrefixOf | Data.SBV.Internals | 
| SeqReplace | Data.SBV.Internals | 
| SeqSubseq | Data.SBV.Internals | 
| SeqSuffixOf | Data.SBV.Internals | 
| SeqUnit | Data.SBV.Internals | 
| setBit | Data.SBV.Trans, Data.SBV | 
| setBitTo | Data.SBV.Trans, Data.SBV | 
| setFlag | Documentation.SBV.Examples.BitPrecise.Legato | 
| SetInfo | Data.SBV.Trans.Control, Data.SBV.Control | 
| setInfo | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| SetLogic | Data.SBV.Trans.Control, Data.SBV.Control | 
| setLogic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| SetOp | Data.SBV.Internals | 
| setOption | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| setReg | Documentation.SBV.Examples.BitPrecise.Legato | 
| setTimeOut | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| setup | Data.SBV.Tools.WeakestPreconditions | 
| Sex | Documentation.SBV.Examples.Puzzles.Murder | 
| sex | Documentation.SBV.Examples.Puzzles.Murder | 
| SExecutable | Data.SBV.Trans, Data.SBV | 
| sExpt | Documentation.SBV.Examples.Queries.FourFours | 
| sExtractBits | Data.SBV.Trans, Data.SBV | 
| sFactorial | Documentation.SBV.Examples.Queries.FourFours | 
| sFalse | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sFemale | Documentation.SBV.Examples.Puzzles.Murder | 
| SFiniteBits | Data.SBV.Trans, Data.SBV | 
| sFiniteBitSize | Data.SBV.Trans, Data.SBV | 
| sFish | Documentation.SBV.Examples.Puzzles.Fish | 
| SFloat | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sFloat |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sFloatAsComparableSWord32 | Data.SBV.Internals | 
| sFloatAsSWord32 | Data.SBV.Trans, Data.SBV | 
| SFloatingPoint | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sFloatingPoint | Data.SBV | 
| sFloatingPointAsComparableSWord | Data.SBV.Internals | 
| sFloatingPointAsSWord | Data.SBV.Trans, Data.SBV | 
| sFloatingPoints | Data.SBV | 
| sFloatingPoint_ | Data.SBV | 
| sFloats |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sFloat_ | Data.SBV | 
| sFootball | Documentation.SBV.Examples.Puzzles.Fish | 
| SFPDouble | Data.SBV.Internals, Data.SBV | 
| sFPDouble | Data.SBV | 
| sFPDoubles | Data.SBV | 
| sFPDouble_ | Data.SBV | 
| SFPHalf | Data.SBV.Internals, Data.SBV | 
| sFPHalf | Data.SBV | 
| sFPHalfs | Data.SBV | 
| sFPHalf_ | Data.SBV | 
| SFPQuad | Data.SBV.Internals, Data.SBV | 
| sFPQuad | Data.SBV | 
| sFPQuads | Data.SBV | 
| sFPQuad_ | Data.SBV | 
| SFPSingle | Data.SBV.Internals, Data.SBV | 
| sFPSingle | Data.SBV | 
| sFPSingles | Data.SBV | 
| sFPSingle_ | Data.SBV | 
| sFri | Documentation.SBV.Examples.Optimization.Enumerate | 
| sFriday | Documentation.SBV.Examples.Queries.Enums | 
| sFromIntegral | Data.SBV.Trans, Data.SBV | 
| sFromIntegralChecked | Data.SBV.Tools.Overflow | 
| sFromIntegralO | Data.SBV.Tools.Overflow | 
| SFunArr | Data.SBV.Dynamic | 
| SFunArray |  | 
| 1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| sgcd | Documentation.SBV.Examples.CodeGeneration.GCD | 
| sgcdIsCorrect | Documentation.SBV.Examples.CodeGeneration.GCD | 
| sGerman | Documentation.SBV.Examples.Puzzles.Fish | 
| sGreen |  | 
| 1 (Function) | Documentation.SBV.Examples.Puzzles.Fish | 
| 2 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle | 
| SHA |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.Crypto.SHA | 
| 2 (Data Constructor) | Documentation.SBV.Examples.Crypto.SHA | 
| sha224 | Documentation.SBV.Examples.Crypto.SHA | 
| sha224P | Documentation.SBV.Examples.Crypto.SHA | 
| sha256 | Documentation.SBV.Examples.Crypto.SHA | 
| sha256P | Documentation.SBV.Examples.Crypto.SHA | 
| sha384 | Documentation.SBV.Examples.Crypto.SHA | 
| sha384P | Documentation.SBV.Examples.Crypto.SHA | 
| sha512 | Documentation.SBV.Examples.Crypto.SHA | 
| sha512P | Documentation.SBV.Examples.Crypto.SHA | 
| sha512_224 | Documentation.SBV.Examples.Crypto.SHA | 
| sha512_224P | Documentation.SBV.Examples.Crypto.SHA | 
| sha512_256 | Documentation.SBV.Examples.Crypto.SHA | 
| sha512_256P | Documentation.SBV.Examples.Crypto.SHA | 
| shaConstants | Documentation.SBV.Examples.Crypto.SHA | 
| shaLoopCount | Documentation.SBV.Examples.Crypto.SHA | 
| shannon | Documentation.SBV.Examples.Uninterpreted.Shannon | 
| shannon2 | Documentation.SBV.Examples.Uninterpreted.Shannon | 
| shaP | Documentation.SBV.Examples.Crypto.SHA | 
| shared | Documentation.SBV.Examples.Queries.Concurrency | 
| sharedDependent | Documentation.SBV.Examples.Queries.Concurrency | 
| sHere | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| shex | Data.SBV.Internals | 
| shexI | Data.SBV.Internals | 
| shift | Data.SBV.Trans, Data.SBV | 
| shiftL | Data.SBV.Trans, Data.SBV | 
| shiftLeft | Documentation.SBV.Examples.CodeGeneration.Uninterpreted | 
| shiftR | Data.SBV.Trans, Data.SBV | 
| Shl | Data.SBV.Internals | 
| sHockey | Documentation.SBV.Examples.Puzzles.Fish | 
| sHorse | Documentation.SBV.Examples.Puzzles.Fish | 
| showBFloat | Data.SBV.Internals | 
| showCDouble | Data.SBV.Internals | 
| showCFloat | Data.SBV.Internals | 
| showFloatAtBase | Data.SBV.Internals | 
| showHash | Documentation.SBV.Examples.Crypto.SHA | 
| showHDouble | Data.SBV.Internals | 
| showHFloat | Data.SBV.Internals | 
| showModel | Data.SBV.Internals | 
| showPoly | Data.SBV.Tools.Polynomial | 
| showPolynomial | Data.SBV.Tools.Polynomial | 
| showSMTDouble | Data.SBV.Internals | 
| showSMTFloat | Data.SBV.Internals | 
| showTDiff | Data.SBV.Internals | 
| showType | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| Shr | Data.SBV.Internals | 
| SHumanHeightInCm | Documentation.SBV.Examples.Misc.Newtypes | 
| SI | Documentation.SBV.Examples.Misc.SetAlgebra | 
| sIdle | Documentation.SBV.Examples.Lists.BoundedMutex | 
| sigma0 | Documentation.SBV.Examples.Crypto.SHA | 
| sigma0Coefficients | Documentation.SBV.Examples.Crypto.SHA | 
| sigma1 | Documentation.SBV.Examples.Crypto.SHA | 
| sigma1Coefficients | Documentation.SBV.Examples.Crypto.SHA | 
| signExtend | Data.SBV.Trans, Data.SBV | 
| sInfinity | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| singleton |  | 
| 1 (Function) | Data.SBV.String | 
| 2 (Function) | Data.SBV.Set | 
| 3 (Function) | Data.SBV.List | 
| SInt | Data.SBV.Trans, Data.SBV | 
| sInt |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| SInt16 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sInt16 |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInt16s |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInt16_ | Data.SBV | 
| SInt32 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sInt32 |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInt32s |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInt32_ | Data.SBV | 
| SInt64 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sInt64 |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInt64s |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInt64_ | Data.SBV | 
| SInt8 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sInt8 |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInt8s |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInt8_ | Data.SBV | 
| SInteger | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sInteger |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sIntegers |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInteger_ | Data.SBV | 
| SIntegral | Data.SBV.Trans, Data.SBV | 
| sIntN | Data.SBV.Dynamic | 
| sIntN_ | Data.SBV.Dynamic | 
| sInts |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sInt_ | Data.SBV | 
| sJust | Data.SBV.Maybe | 
| sKiller | Documentation.SBV.Examples.Puzzles.Murder | 
| Skip | Data.SBV.Tools.WeakestPreconditions | 
| SL | Documentation.SBV.Examples.Uninterpreted.UISortAllSat | 
| sLarry | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| sLeft | Data.SBV.Either | 
| SList | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sList |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sListArray | Data.SBV.Internals, Data.SBV | 
| sLists |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sList_ | Data.SBV | 
| SLocation |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Murder | 
| 2 (Type/Class) | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| sMale | Documentation.SBV.Examples.Puzzles.Murder | 
| smax | Data.SBV.Trans, Data.SBV | 
| SMaybe | Data.SBV.Internals, Data.SBV | 
| sMaybe | Data.SBV | 
| sMaybes | Data.SBV | 
| sMaybe_ | Data.SBV | 
| SMetres | Documentation.SBV.Examples.Misc.Newtypes | 
| sMilk | Documentation.SBV.Examples.Puzzles.Fish | 
| smin | Data.SBV.Trans, Data.SBV | 
| sMinus | Documentation.SBV.Examples.Queries.FourFours | 
| sMod | Data.SBV.Trans, Data.SBV | 
| sMon | Documentation.SBV.Examples.Optimization.Enumerate | 
| sMonday | Documentation.SBV.Examples.Queries.Enums | 
| SMTConfig |  | 
| 1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| 2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| SMTErrorBehavior | Data.SBV.Trans.Control, Data.SBV.Control | 
| SMTInfoFlag | Data.SBV.Trans.Control, Data.SBV.Control | 
| SMTInfoResponse | Data.SBV.Trans.Control, Data.SBV.Control | 
| SMTLib2 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| SMTLibPgm |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| smtLibPgm | Data.SBV.Internals | 
| smtLibReservedNames | Data.SBV.Internals | 
| SMTLibVersion | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| smtLibVersion | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| smtLibVersionExtension | Data.SBV.Internals | 
| SMTMode | Data.SBV.Internals | 
| SMTModel |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| SMTOption | Data.SBV.Trans.Control, Data.SBV.Control | 
| SMTProblem |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| SMTReasonUnknown | Data.SBV.Trans, Data.SBV | 
| SMTResult | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| smtRoundingMode | Data.SBV.Internals | 
| SMTScript |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| SMTSolver |  | 
| 1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| 2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| SMTVerbosity | Data.SBV.Trans.Control, Data.SBV.Control | 
| sName |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sName_ |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sNaN | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| SNationality | Documentation.SBV.Examples.Puzzles.Fish | 
| sNegate | Documentation.SBV.Examples.Queries.FourFours | 
| snoc |  | 
| 1 (Function) | Data.SBV.String | 
| 2 (Function) | Data.SBV.List | 
| sNorwegian | Documentation.SBV.Examples.Puzzles.Fish | 
| sNot | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sNotElem | Data.SBV.Trans, Data.SBV | 
| sNothing | Data.SBV.Maybe | 
| sObserve | Data.SBV | 
| softConstrain | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| Solution |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.Existentials.Diophantine | 
| 2 (Type/Class) | Documentation.SBV.Examples.Puzzles.NQueens | 
| solve |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| solveAll | Documentation.SBV.Examples.Puzzles.Sudoku | 
| solveCrossword | Documentation.SBV.Examples.Strings.RegexCrossword | 
| solveEuler185 | Documentation.SBV.Examples.Puzzles.Euler185 | 
| solveN | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| Solver | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| solver | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| SolverCapabilities |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| SolverContext | Data.SBV.Internals | 
| solverSetOptions | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| solveU2 | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| sOr | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| SPet | Documentation.SBV.Examples.Puzzles.Fish | 
| sPlus | Documentation.SBV.Examples.Queries.FourFours | 
| sPopCount | Data.SBV.Trans, Data.SBV | 
| Sport | Documentation.SBV.Examples.Puzzles.Fish | 
| SQ | Documentation.SBV.Examples.Uninterpreted.Sort | 
| SQLExpr | Documentation.SBV.Examples.Strings.SQLInjection | 
| Sqrt | Documentation.SBV.Examples.Queries.FourFours | 
| sqrt | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt | 
| SqrtS |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt | 
| 2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt | 
| sQuot | Data.SBV.Trans, Data.SBV | 
| sQuotRem | Data.SBV.Trans, Data.SBV | 
| sReady | Documentation.SBV.Examples.Lists.BoundedMutex | 
| SReal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sReal |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sReals |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sRealToSInteger | Data.SBV.Trans, Data.SBV | 
| sReal_ | Data.SBV | 
| sRed |  | 
| 1 (Function) | Documentation.SBV.Examples.Puzzles.Fish | 
| 2 (Function) | Documentation.SBV.Examples.Puzzles.Garden | 
| 3 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle | 
| sRem | Data.SBV.Trans, Data.SBV | 
| sRight | Data.SBV.Either | 
| sRNA | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sRNE | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| SRole | Documentation.SBV.Examples.Puzzles.Murder | 
| sRotateLeft | Data.SBV.Trans, Data.SBV | 
| sRotateRight | Data.SBV.Trans, Data.SBV | 
| SRoundingMode | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sRoundNearestTiesToAway | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sRoundNearestTiesToEven | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sRoundTowardNegative | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sRoundTowardPositive | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sRoundTowardZero | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sRTN | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sRTP | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sRTZ | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sSat | Documentation.SBV.Examples.Optimization.Enumerate | 
| sSaturday | Documentation.SBV.Examples.Queries.Enums | 
| SSet | Data.SBV.Internals, Data.SBV | 
| sSet | Data.SBV | 
| sSets | Data.SBV | 
| sSet_ | Data.SBV | 
| SSex | Documentation.SBV.Examples.Puzzles.Murder | 
| sShiftLeft | Data.SBV.Trans, Data.SBV | 
| sShiftRight | Data.SBV.Trans, Data.SBV | 
| sSignedShiftArithRight | Data.SBV.Trans, Data.SBV | 
| SSport | Documentation.SBV.Examples.Puzzles.Fish | 
| sSqrt | Documentation.SBV.Examples.Queries.FourFours | 
| SState | Documentation.SBV.Examples.Lists.BoundedMutex | 
| SString | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sString |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sStrings |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sString_ | Data.SBV | 
| sSun | Documentation.SBV.Examples.Optimization.Enumerate | 
| sSunday | Documentation.SBV.Examples.Queries.Enums | 
| sSwede | Documentation.SBV.Examples.Puzzles.Fish | 
| stability | Data.SBV.Tools.WeakestPreconditions | 
| Stable | Data.SBV.Tools.WeakestPreconditions | 
| stable | Data.SBV.Tools.WeakestPreconditions | 
| start | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| State |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Type/Class) | Documentation.SBV.Examples.Crypto.AES | 
| 3 (Type/Class) | Documentation.SBV.Examples.Lists.BoundedMutex | 
| statementRe | Documentation.SBV.Examples.Strings.SQLInjection | 
| Status |  | 
| 1 (Type/Class) | Data.SBV.Tools.WeakestPreconditions | 
| 2 (Type/Class) | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| 3 (Data Constructor) | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| sTea | Documentation.SBV.Examples.Puzzles.Fish | 
| sTennis | Documentation.SBV.Examples.Puzzles.Fish | 
| sTestBit | Data.SBV.Trans, Data.SBV | 
| sThere | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| sThu | Documentation.SBV.Examples.Optimization.Enumerate | 
| sThursday | Documentation.SBV.Examples.Queries.Enums | 
| STime | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| sTimes | Documentation.SBV.Examples.Queries.FourFours | 
| Stmt | Data.SBV.Tools.WeakestPreconditions | 
| StrConcat | Data.SBV.Internals | 
| StrContains | Data.SBV.Internals | 
| STree | Data.SBV.Tools.STree | 
| StrFromCode | Data.SBV.Internals | 
| StrIndexOf | Data.SBV.Internals | 
| StrInRe | Data.SBV.Internals | 
| StrLen | Data.SBV.Internals | 
| StrNatToStr | Data.SBV.Internals | 
| StrNth | Data.SBV.Internals | 
| StrOp |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| StrPrefixOf | Data.SBV.Internals | 
| strRe | Documentation.SBV.Examples.Strings.SQLInjection | 
| StrReplace | Data.SBV.Internals | 
| StrStrToNat | Data.SBV.Internals | 
| StrSubstr | Data.SBV.Internals | 
| StrSuffixOf | Data.SBV.Internals | 
| strToCharAt | Data.SBV.String | 
| StrToCode | Data.SBV.Internals | 
| strToNat | Data.SBV.String | 
| strToStrAt | Data.SBV.String | 
| sTrue | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| StrUnit | Data.SBV.Internals | 
| Stuck | Data.SBV.Tools.WeakestPreconditions | 
| sTue | Documentation.SBV.Examples.Optimization.Enumerate | 
| sTuesday | Documentation.SBV.Examples.Queries.Enums | 
| STuple | Data.SBV.Internals, Data.SBV | 
| sTuple | Data.SBV | 
| STuple2 | Data.SBV.Internals, Data.SBV | 
| STuple3 | Data.SBV.Internals, Data.SBV | 
| STuple4 | Data.SBV.Internals, Data.SBV | 
| STuple5 | Data.SBV.Internals, Data.SBV | 
| STuple6 | Data.SBV.Internals, Data.SBV | 
| STuple7 | Data.SBV.Internals, Data.SBV | 
| STuple8 | Data.SBV.Internals, Data.SBV | 
| sTuples | Data.SBV | 
| sTuple_ | Data.SBV | 
| SU2Member | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| subList | Data.SBV.List | 
| subStr | Data.SBV.String | 
| sudoku | Documentation.SBV.Examples.Puzzles.Sudoku | 
| sum0 | Documentation.SBV.Examples.Crypto.SHA | 
| sum0Coefficients | Documentation.SBV.Examples.Crypto.SHA | 
| sum1 | Documentation.SBV.Examples.Crypto.SHA | 
| sum1Coefficients | Documentation.SBV.Examples.Crypto.SHA | 
| sumCorrect | Documentation.SBV.Examples.ProofTools.Sum | 
| SumS |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Sum | 
| 2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Sum | 
| Sun | Documentation.SBV.Examples.Optimization.Enumerate | 
| Sunday | Documentation.SBV.Examples.Queries.Enums | 
| SUnOp | Documentation.SBV.Examples.Queries.FourFours | 
| supportsApproxReals | Data.SBV.Internals | 
| supportsBitVectors | Data.SBV.Internals | 
| supportsCustomQueries | Data.SBV.Internals | 
| supportsDataTypes | Data.SBV.Internals | 
| supportsDefineFun | Data.SBV.Internals | 
| supportsDeltaSat | Data.SBV.Internals | 
| supportsDirectAccessors | Data.SBV.Internals | 
| supportsDistinct | Data.SBV.Internals | 
| supportsFlattenedModels | Data.SBV.Internals | 
| supportsGlobalDecls | Data.SBV.Internals | 
| supportsIEEE754 | Data.SBV.Internals | 
| supportsInt2bv | Data.SBV.Internals | 
| supportsOptimization | Data.SBV.Internals | 
| supportsPseudoBooleans | Data.SBV.Internals | 
| supportsQuantifiers | Data.SBV.Internals | 
| supportsReals | Data.SBV.Internals | 
| supportsSets | Data.SBV.Internals | 
| supportsUnboundedInts | Data.SBV.Internals | 
| supportsUninterpretedSorts | Data.SBV.Internals | 
| SV |  | 
| 1 (Type/Class) | Data.SBV.Internals | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| svAbs | Data.SBV.Dynamic | 
| svAddConstant | Data.SBV.Dynamic | 
| SVal |  | 
| 1 (Type/Class) | Data.SBV.Internals, Data.SBV.Dynamic | 
| 2 (Data Constructor) | Data.SBV.Internals | 
| svAnd | Data.SBV.Dynamic | 
| svAsBool | Data.SBV.Dynamic | 
| svAsInteger | Data.SBV.Dynamic | 
| svBarrelRotateLeft | Data.SBV.Dynamic | 
| svBarrelRotateRight | Data.SBV.Dynamic | 
| svBlastBE | Data.SBV.Dynamic | 
| svBlastLE | Data.SBV.Dynamic | 
| svBool | Data.SBV.Dynamic | 
| svCgInput | Data.SBV.Internals, Data.SBV.Dynamic | 
| svCgInputArr | Data.SBV.Internals, Data.SBV.Dynamic | 
| svCgOutput | Data.SBV.Internals, Data.SBV.Dynamic | 
| svCgOutputArr | Data.SBV.Internals, Data.SBV.Dynamic | 
| svCgReturn | Data.SBV.Internals, Data.SBV.Dynamic | 
| svCgReturnArr | Data.SBV.Internals, Data.SBV.Dynamic | 
| svDecrement | Data.SBV.Dynamic | 
| svDenominator | Data.SBV.Dynamic | 
| svDivide | Data.SBV.Dynamic | 
| svDouble | Data.SBV.Dynamic | 
| svEnumFromThenTo | Data.SBV.Dynamic | 
| svEqual | Data.SBV.Dynamic | 
| svExp | Data.SBV.Dynamic | 
| svExtract | Data.SBV.Dynamic | 
| svFalse | Data.SBV.Dynamic | 
| svFloat | Data.SBV.Dynamic | 
| svFloatingPoint | Data.SBV.Dynamic | 
| svFromIntegral | Data.SBV.Dynamic | 
| svFromWord1 | Data.SBV.Dynamic | 
| svGreaterEq | Data.SBV.Dynamic | 
| svGreaterThan | Data.SBV.Dynamic | 
| sVictim | Documentation.SBV.Examples.Puzzles.Murder | 
| svIncrement | Data.SBV.Dynamic | 
| svInteger | Data.SBV.Dynamic | 
| svIte | Data.SBV.Dynamic | 
| svJoin | Data.SBV.Dynamic | 
| svLazyIte | Data.SBV.Dynamic | 
| svLessEq | Data.SBV.Dynamic | 
| svLessThan | Data.SBV.Dynamic | 
| svMinus | Data.SBV.Dynamic | 
| svMkSymVar | Data.SBV.Dynamic | 
| svNot | Data.SBV.Dynamic | 
| svNotEqual | Data.SBV.Dynamic | 
| svNumerator | Data.SBV.Dynamic | 
| sVolleyball | Documentation.SBV.Examples.Puzzles.Fish | 
| svOr | Data.SBV.Dynamic | 
| svPlus | Data.SBV.Dynamic | 
| svQuickCheck | Data.SBV.Dynamic | 
| svQuot | Data.SBV.Dynamic | 
| svQuotRem | Data.SBV.Dynamic | 
| svReal | Data.SBV.Dynamic | 
| svRem | Data.SBV.Dynamic | 
| svRol | Data.SBV.Dynamic | 
| svRor | Data.SBV.Dynamic | 
| svRotateLeft | Data.SBV.Dynamic | 
| svRotateRight | Data.SBV.Dynamic | 
| svSelect | Data.SBV.Dynamic | 
| svSetBit | Data.SBV.Dynamic | 
| svShiftLeft | Data.SBV.Dynamic | 
| svShiftRight | Data.SBV.Dynamic | 
| svShl | Data.SBV.Dynamic | 
| svShr | Data.SBV.Dynamic | 
| svSign | Data.SBV.Dynamic | 
| svStructuralLessThan | Data.SBV.Dynamic | 
| svSymbolicMerge | Data.SBV.Dynamic | 
| svTestBit | Data.SBV.Dynamic | 
| svTimes | Data.SBV.Dynamic | 
| svToWord1 | Data.SBV.Dynamic | 
| svTrue | Data.SBV.Dynamic | 
| svUNeg | Data.SBV.Dynamic | 
| svUninterpreted | Data.SBV.Dynamic | 
| svUnsign | Data.SBV.Dynamic | 
| svWordFromBE | Data.SBV.Dynamic | 
| svWordFromLE | Data.SBV.Dynamic | 
| svXOr | Data.SBV.Dynamic | 
| swap | Documentation.SBV.Examples.Crypto.RC4 | 
| sWater | Documentation.SBV.Examples.Puzzles.Fish | 
| sWed | Documentation.SBV.Examples.Optimization.Enumerate | 
| Swede | Documentation.SBV.Examples.Puzzles.Fish | 
| sWednesday | Documentation.SBV.Examples.Queries.Enums | 
| sWhite | Documentation.SBV.Examples.Puzzles.Fish | 
| SWord | Data.SBV.Trans, Data.SBV | 
| sWord |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| SWord16 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sWord16 |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sWord16s |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sWord16_ | Data.SBV | 
| SWord32 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sWord32 |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sWord32AsSFloat | Data.SBV.Trans, Data.SBV | 
| sWord32s |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sWord32_ | Data.SBV | 
| SWord64 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sWord64 |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sWord64AsSDouble | Data.SBV.Trans, Data.SBV | 
| sWord64s |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sWord64_ | Data.SBV | 
| SWord8 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| sWord8 |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sWord8s |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sWord8_ | Data.SBV | 
| sWordAsSFloatingPoint | Data.SBV.Trans, Data.SBV | 
| sWordN | Data.SBV.Dynamic | 
| sWordN_ | Data.SBV.Dynamic | 
| sWords |  | 
| 1 (Function) | Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| sWord_ | Data.SBV | 
| sYellow |  | 
| 1 (Function) | Documentation.SBV.Examples.Puzzles.Fish | 
| 2 (Function) | Documentation.SBV.Examples.Puzzles.Garden | 
| sym | Data.SBV.Trans, Data.SBV | 
| SymArray | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| Symbolic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| symbolic |  | 
| 1 (Function) | Data.SBV.Internals, Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| symbolicEnv | Data.SBV.Trans, Data.SBV | 
| symbolicMerge | Data.SBV.Trans, Data.SBV | 
| symbolics |  | 
| 1 (Function) | Data.SBV.Internals, Data.SBV.Trans | 
| 2 (Function) | Data.SBV | 
| SymbolicT | Data.SBV.Trans, Data.SBV | 
| SymTuple | Data.SBV | 
| SymVal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| synthMul22 | Documentation.SBV.Examples.Uninterpreted.Multiply |