| k |  | 
| 1 (Function) | Documentation.SBV.Examples.ProofTools.Fibonacci | 
| 2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib | 
| KBool | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KBounded | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KChar | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KDouble | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KEither | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| Key |  | 
| 1 (Type/Class) | Documentation.SBV.Examples.Crypto.AES | 
| 2 (Type/Class) | Documentation.SBV.Examples.Crypto.RC4 | 
| keyExpansion | Documentation.SBV.Examples.Crypto.AES | 
| keySchedule | Documentation.SBV.Examples.Crypto.RC4 | 
| keyScheduleString | Documentation.SBV.Examples.Crypto.RC4 | 
| KFloat | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KFP | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| Killer | Documentation.SBV.Examples.Puzzles.Murder | 
| killer | Documentation.SBV.Examples.Puzzles.Murder | 
| Kind | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KindCast | Data.SBV.Internals | 
| kindOf | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KList | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KMaybe | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| knownAnswerTests | Documentation.SBV.Examples.Crypto.SHA | 
| KPlus | Data.SBV.RegExp, Data.SBV.Internals | 
| KReal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KS | Documentation.SBV.Examples.Crypto.AES | 
| KSet | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KStar | Data.SBV.RegExp, Data.SBV.Internals | 
| KString | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KTuple | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KUnbounded | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic | 
| KUserSort | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |