| M | Documentation.SBV.Examples.Strings.SQLInjection |
| m | |
| 1 (Function) | Documentation.SBV.Examples.ProofTools.Fibonacci |
| 2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib |
| magic | Documentation.SBV.Examples.Puzzles.MagicSquare |
| maj | Documentation.SBV.Examples.Crypto.SHA |
| Male | Documentation.SBV.Examples.Puzzles.Murder |
| map | Data.SBV.Maybe |
| mapCV | Data.SBV.Internals |
| mapCV2 | Data.SBV.Internals |
| maskAndMult | Documentation.SBV.Examples.BitPrecise.MultMask |
| match | Data.SBV.RegExp |
| MathSAT | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| mathSAT | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| maxE | Documentation.SBV.Examples.Misc.Enumerate |
| Maximize | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| maximize | Data.SBV |
| may | Documentation.SBV.Examples.Puzzles.Birthday |
| maybe | Data.SBV.Maybe |
| MaybeAccess | Data.SBV.Internals |
| MaybeConstructor | Data.SBV.Internals |
| MaybeIs | Data.SBV.Internals |
| mdp | Data.SBV.Tools.Polynomial |
| Measure | Data.SBV.Tools.WeakestPreconditions |
| measure | |
| 1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv |
| 2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt |
| 3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length |
| MeasureBound | Data.SBV.Tools.WeakestPreconditions |
| MeasureDecrease | Data.SBV.Tools.WeakestPreconditions |
| member | Data.SBV.Set |
| Memory | Documentation.SBV.Examples.BitPrecise.Legato |
| memory | Documentation.SBV.Examples.BitPrecise.Legato |
| merge | Documentation.SBV.Examples.BitPrecise.MergeSort |
| Mergeable | Data.SBV.Trans, Data.SBV |
| mergeArrays | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| mergeSArr | Data.SBV.Dynamic |
| mergeSFunArr | Data.SBV.Dynamic |
| mergeSort | Documentation.SBV.Examples.BitPrecise.MergeSort |
| Metres | |
| 1 (Type/Class) | Documentation.SBV.Examples.Misc.Newtypes |
| 2 (Data Constructor) | Documentation.SBV.Examples.Misc.Newtypes |
| Metric | Data.SBV.Trans, Data.SBV |
| MetricSpace | Data.SBV.Trans, Data.SBV |
| midPointAlternative | Documentation.SBV.Examples.BitPrecise.BrokenSearch |
| midPointBroken | Documentation.SBV.Examples.BitPrecise.BrokenSearch |
| midPointFixed | Documentation.SBV.Examples.BitPrecise.BrokenSearch |
| Milk | Documentation.SBV.Examples.Puzzles.Fish |
| minE | Documentation.SBV.Examples.Misc.Enumerate |
| Minimize | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| minimize | Data.SBV |
| Minus | |
| 1 (Data Constructor) | Data.SBV.Internals |
| 2 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours |
| mkCoin | Documentation.SBV.Examples.Puzzles.Coins |
| mkConstCV | Data.SBV.Internals |
| mkExistVars | |
| 1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| mkFibs | Documentation.SBV.Examples.Lists.Fibonacci |
| mkForallVars | |
| 1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| mkFreeVars | |
| 1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| mkQuery | Documentation.SBV.Examples.Transformers.SymbolicEval |
| mkResult | Documentation.SBV.Examples.Transformers.SymbolicEval |
| mkSkolemZero | Data.SBV.Internals |
| mkSMTResult | |
| 1 (Function) | Data.SBV.Trans.Control |
| 2 (Function) | Data.SBV.Control |
| mkSTree | Data.SBV.Tools.STree |
| mkSymbolicEnumeration | Data.SBV.Trans, Data.SBV |
| mkSymSBV | Data.SBV.Internals |
| mkSymVal | |
| 1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| mkUninterpretedSort | Data.SBV.Trans, Data.SBV |
| Modelable | Data.SBV.Trans, Data.SBV |
| modelAssocs | Data.SBV.Internals |
| modelBindings | Data.SBV.Internals |
| modelExists | Data.SBV.Trans, Data.SBV |
| modelObjectives | Data.SBV.Internals |
| modelsWithYAux | Documentation.SBV.Examples.Misc.Auxiliary |
| modelUIFuns | Data.SBV.Internals |
| Mon | Documentation.SBV.Examples.Optimization.Enumerate |
| MonadQuery | Data.SBV.Trans.Control, Data.SBV.Control |
| MonadSymbolic | Data.SBV.Trans, Data.SBV |
| Monday | Documentation.SBV.Examples.Queries.Enums |
| Month | Documentation.SBV.Examples.Puzzles.Birthday |
| Mostek | |
| 1 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato |
| 2 (Data Constructor) | Documentation.SBV.Examples.BitPrecise.Legato |
| Move | Documentation.SBV.Examples.Puzzles.U2Bridge |
| move1 | Documentation.SBV.Examples.Puzzles.U2Bridge |
| move2 | Documentation.SBV.Examples.Puzzles.U2Bridge |
| MProvable | Data.SBV.Trans |
| msb | Data.SBV.Trans, Data.SBV |
| msMaximize | Data.SBV.Trans, Data.SBV |
| msMinimize | Data.SBV.Trans, Data.SBV |
| mul22 | Documentation.SBV.Examples.Uninterpreted.Multiply |
| MulExtCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| multAssoc | Documentation.SBV.Examples.Misc.Polynomials |
| multComm | Documentation.SBV.Examples.Misc.Polynomials |
| multInverse | Documentation.SBV.Examples.Misc.Floating |
| multUnit | Documentation.SBV.Examples.Misc.Polynomials |
| mutex | Documentation.SBV.Examples.Lists.BoundedMutex |