Index - I
| inclusion | |
| 1 (Function) | Data.Type.Ordinal |
| 2 (Function) | Data.Type.Ordinal.Builtin |
| 3 (Function) | Data.Type.Ordinal.Peano |
| inclusion' | |
| 1 (Function) | Data.Type.Ordinal |
| 2 (Function) | Data.Type.Ordinal.Builtin |
| 3 (Function) | Data.Type.Ordinal.Peano |
| induction | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| inductionNat | Data.Type.Natural.Builtin |
| intToNat | Data.Type.Natural |
| IsPeano | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| IsSucc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
| IsZero | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |