| Objective | Data.SBV.Trans, Data.SBV.Internals, Data.SBV |
| observe | Data.SBV.Trans, Data.SBV |
| observeIf | Data.SBV |
| octal | Data.SBV.RegExp |
| octDigit | Data.SBV.RegExp |
| offsetIndexOf | |
| 1 (Function) | Data.SBV.String |
| 2 (Function) | Data.SBV.List |
| oneIf | Data.SBV.Trans, Data.SBV |
| oneOf | Data.SBV.RegExp |
| Op | Data.SBV.Internals |
| Open | Data.SBV.Tools.Range |
| 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.Trans, Data.SBV.Internals, Data.SBV |
| optimizeValidateConstraints | Data.SBV.Trans, Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic |
| optimizeWith | |
| 1 (Function) | Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| OptionKeyword | Data.SBV.Trans.Control, Data.SBV.Control |
| options | Data.SBV.Trans, Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic |
| Or | |
| 1 (Data Constructor) | Data.SBV.Internals |
| 2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval |
| or | Documentation.SBV.Examples.Uninterpreted.Deduce |
| ord | Data.SBV.Char |
| OrdSymbolic | Data.SBV.Trans, Data.SBV |
| output | |
| 1 (Function) | Data.SBV.Trans, Data.SBV.Internals |
| 2 (Function) | Data.SBV |
| outputSVal | Data.SBV.Dynamic |
| Outputtable | Data.SBV.Internals |
| outside | Documentation.SBV.Examples.Misc.ModelExtract |
| OverflowOp | Data.SBV.Internals |