| L | Documentation.SBV.Examples.Uninterpreted.UISortAllSat |
| l | Documentation.SBV.Examples.WeakestPreconditions.Length |
| Label | Data.SBV.Internals |
| label | Data.SBV.Trans, Data.SBV |
| lAdam | Documentation.SBV.Examples.Puzzles.U2Bridge |
| ladyAndTigers | Documentation.SBV.Examples.Puzzles.LadyAndTigers |
| Lam | Documentation.SBV.Examples.ADT.Types |
| Lambda | Data.SBV.Internals |
| lambda | Data.SBV.Internals |
| lambdaArray | Data.SBV |
| lambdaEUFExprFun | Documentation.SBV.Examples.Uninterpreted.EUFLogic |
| LambdaGen | Data.SBV.Internals |
| LambdaScope | Data.SBV.Internals |
| lambdaStr | Data.SBV.Internals |
| largerIntegerExists | Documentation.SBV.Examples.TP.Basics |
| Larry | Documentation.SBV.Examples.Puzzles.U2Bridge |
| last | Data.SBV.List |
| lbody | Documentation.SBV.Examples.TP.VM |
| lBono | Documentation.SBV.Examples.Puzzles.U2Bridge |
| ld | Documentation.SBV.Examples.TP.Primes |
| lda | Documentation.SBV.Examples.BitPrecise.Legato |
| ldn | Documentation.SBV.Examples.Existentials.Diophantine |
| ldx | Documentation.SBV.Examples.BitPrecise.Legato |
| leastDivisorDivides | Documentation.SBV.Examples.TP.Primes |
| leastDivisorIsLeast | Documentation.SBV.Examples.TP.Primes |
| leastDivisorIsPrime | Documentation.SBV.Examples.TP.Primes |
| leastDivisorTwice | Documentation.SBV.Examples.TP.Primes |
| leastPrimeDivisor | Documentation.SBV.Examples.TP.Primes |
| lEdge | Documentation.SBV.Examples.Puzzles.U2Bridge |
| legato | Documentation.SBV.Examples.BitPrecise.Legato |
| legatoInC | Documentation.SBV.Examples.BitPrecise.Legato |
| legatoIsCorrect | Documentation.SBV.Examples.BitPrecise.Legato |
| lemma | Data.SBV.TP |
| lemmaWith | Data.SBV.TP |
| len | Documentation.SBV.Examples.Misc.Definitions |
| lenAppend | Documentation.SBV.Examples.TP.Lists |
| lenAppend2 | Documentation.SBV.Examples.TP.Lists |
| lenExample | Documentation.SBV.Examples.Misc.Definitions |
| length | Data.SBV.List |
| lengthTail | Documentation.SBV.Examples.TP.Lists |
| length_drop | Documentation.SBV.Examples.TP.Lists |
| length_take | Documentation.SBV.Examples.TP.Lists |
| LenS | |
| 1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Length |
| 2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Length |
| LessEq | Data.SBV.Internals |
| LessThan | |
| 1 (Data Constructor) | Data.SBV.Internals |
| 2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval |
| Let | |
| 1 (Data Constructor) | Documentation.SBV.Examples.ADT.Expr |
| 2 (Data Constructor) | Documentation.SBV.Examples.ADT.Param |
| 3 (Data Constructor) | Documentation.SBV.Examples.TP.VM |
| letHelper | Documentation.SBV.Examples.TP.ConstFold |
| Lexicographic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| LexicographicResult | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| le_antisymm | Documentation.SBV.Examples.TP.ShefferStroke |
| le_inf | Documentation.SBV.Examples.TP.ShefferStroke |
| le_refl | Documentation.SBV.Examples.TP.ShefferStroke |
| le_sup_inf | Documentation.SBV.Examples.TP.ShefferStroke |
| le_sup_left | Documentation.SBV.Examples.TP.ShefferStroke |
| le_sup_right | Documentation.SBV.Examples.TP.ShefferStroke |
| le_top | Documentation.SBV.Examples.TP.ShefferStroke |
| le_trans | Documentation.SBV.Examples.TP.ShefferStroke |
| lf | Documentation.SBV.Examples.BitPrecise.PrefixSum |
| liftDMod | Data.SBV.Internals |
| liftEither | Data.SBV.Either |
| liftMaybe | Data.SBV.Maybe |
| liftQRem | Data.SBV.Internals |
| listArray | Data.SBV |
| listEq | Data.SBV.List |
| listToListAt | Data.SBV.List |
| Lit | Documentation.SBV.Examples.Transformers.SymbolicEval |
| Literal | Data.SBV.RegExp, Data.SBV.Internals |
| literal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| LkUp | Data.SBV.Internals |
| lLarry | Documentation.SBV.Examples.Puzzles.U2Bridge |
| LO | Documentation.SBV.Examples.BitPrecise.Legato |
| Location | |
| 1 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato |
| 2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Murder |
| 3 (Type/Class) | Documentation.SBV.Examples.Puzzles.Orangutans |
| 4 (Type/Class) | Documentation.SBV.Examples.Puzzles.U2Bridge |
| location | |
| 1 (Function) | Documentation.SBV.Examples.Puzzles.Murder |
| 2 (Function) | Documentation.SBV.Examples.Puzzles.Orangutans |
| Logic | Data.SBV.Trans, Data.SBV |
| Logic_ALL | Data.SBV.Trans, Data.SBV |
| Logic_NONE | Data.SBV.Trans, Data.SBV |
| lookUp | Documentation.SBV.Examples.TP.TautologyChecker |
| lookup | Data.SBV.List |
| lookUpExtends | Documentation.SBV.Examples.TP.TautologyChecker |
| lookUpSame | Documentation.SBV.Examples.TP.TautologyChecker |
| lookupShadow | Documentation.SBV.Examples.TP.ConstFold |
| lookupShadowPfx | Documentation.SBV.Examples.TP.ConstFold |
| lookUpStable | Documentation.SBV.Examples.TP.TautologyChecker |
| lookupSwap | Documentation.SBV.Examples.TP.ConstFold |
| lookupSwapPfx | Documentation.SBV.Examples.TP.ConstFold |
| Loop | Data.SBV.RegExp, Data.SBV.Internals |
| LRA | Data.SBV.Trans, Data.SBV |
| lsb | Data.SBV.Trans, Data.SBV |
| lteEquiv | Documentation.SBV.Examples.TP.Peano |
| ltIrreflexive | Documentation.SBV.Examples.TP.Peano |
| ltTrans | Documentation.SBV.Examples.TP.Peano |
| lt_iff_le_not_le | Documentation.SBV.Examples.TP.ShefferStroke |
| lval | Documentation.SBV.Examples.TP.VM |
| lvar | Documentation.SBV.Examples.TP.VM |