| 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 | 
| Larry | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| lBono | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| lda | Documentation.SBV.Examples.BitPrecise.Legato | 
| ldn | Documentation.SBV.Examples.Existentials.Diophantine | 
| ldx | Documentation.SBV.Examples.BitPrecise.Legato | 
| lEdge | Documentation.SBV.Examples.Puzzles.U2Bridge | 
| legato | Documentation.SBV.Examples.BitPrecise.Legato | 
| legatoInC | Documentation.SBV.Examples.BitPrecise.Legato | 
| legatoIsCorrect | Documentation.SBV.Examples.BitPrecise.Legato | 
| LenC |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Length | 
| 2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Length | 
| length |  | 
| 1 (Function) | Data.SBV.String | 
| 2 (Function) | Data.SBV.List | 
| 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 | 
| Lexicographic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV | 
| LexicographicResult | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| lf | Documentation.SBV.Examples.BitPrecise.PrefixSum | 
| liftCV2 | Data.SBV.Internals | 
| liftDMod | Data.SBV.Internals | 
| liftEither | Data.SBV.Either | 
| liftMaybe | Data.SBV.Maybe | 
| liftQRem | Data.SBV.Internals | 
| 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.U2Bridge | 
| location | Documentation.SBV.Examples.Puzzles.Murder | 
| Logic | Data.SBV.Trans, Data.SBV | 
| Logic_ALL | Data.SBV.Trans, Data.SBV | 
| Logic_NONE | Data.SBV.Trans, Data.SBV | 
| Loop | Data.SBV.RegExp, Data.SBV.Internals | 
| LRA | Data.SBV.Trans, Data.SBV | 
| lsb | Data.SBV.Trans, Data.SBV |