| Objective | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| observe | Data.SBV.Trans, Data.SBV |
| observeIf | Data.SBV |
| octal | Data.SBV.RegExp |
| octDigit | Data.SBV.RegExp |
| oddSequence1 | Documentation.SBV.Examples.KnuckleDragger.StrongInduction |
| oddSequence2 | Documentation.SBV.Examples.KnuckleDragger.StrongInduction |
| Ofallo | Documentation.SBV.Examples.Puzzles.Orangutans |
| offsetIndexOf | |
| 1 (Function) | Data.SBV.String |
| 2 (Function) | Data.SBV.List |
| old | Documentation.SBV.Examples.Puzzles.Rabbits |
| oneBits | Data.SBV.Trans, Data.SBV |
| oneIf | Data.SBV.Trans, Data.SBV |
| oneOf | Data.SBV.RegExp |
| Op | Data.SBV.Internals |
| Open | Data.SBV.Tools.Range |
| OpenPoint | Data.SBV |
| OpenSMT | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| openSMT | Data.SBV |
| oppositeSignsCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks |
| Opt | Data.SBV.RegExp, Data.SBV.Internals |
| optimize | |
| 1 (Function) | Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| OptimizeResult | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| OptimizeStyle | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| optimizeValidateConstraints | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| optimizeWith | |
| 1 (Function) | Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| optIndependent | Data.SBV |
| optIndependentWith | Data.SBV |
| OptionKeyword | Data.SBV.Trans.Control, Data.SBV.Control |
| options | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| optLexicographic | Data.SBV |
| optLexicographicWith | Data.SBV |
| optPareto | Data.SBV |
| optParetoWith | Data.SBV |
| Or | |
| 1 (Data Constructor) | Data.SBV.Internals |
| 2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval |
| or | |
| 1 (Function) | Data.SBV.List |
| 2 (Function) | Documentation.SBV.Examples.Uninterpreted.Deduce |
| Orangutan | Documentation.SBV.Examples.Puzzles.Orangutans |
| orangutan | Documentation.SBV.Examples.Puzzles.Orangutans |
| ord | Data.SBV.Char |
| OrdSymbolic | Data.SBV.Trans, Data.SBV |
| outOfInit | Documentation.SBV.Examples.Misc.LambdaArray |
| output | |
| 1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| outputSVal | Data.SBV.Dynamic |
| Outputtable | Data.SBV.Internals |
| outside | Documentation.SBV.Examples.Misc.ModelExtract |
| OverflowOp | Data.SBV.Internals |
| OvOp | Data.SBV.Internals |