| Peano | Data.Type.Natural.Builtin |
| PeanoOrder | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| PEq | Data.Type.Natural.Builtin |
| plusAssoc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusCancelLeqL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| plusCancelLeqR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| plusComm | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusCong | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
| plusCongL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
| plusCongR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
| plusEqCancelL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusEqCancelR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusEqZeroL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusEqZeroR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusInjectiveL | Data.Type.Natural |
| plusInjectiveR | Data.Type.Natural |
| plusLeqL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| plusLeqR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| plusMinus | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusMinus' | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusMinusEqL | Data.Type.Natural |
| plusMonotone | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| plusMonotoneL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| plusMonotoneR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| plusMultDistrib | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusNeutralL | Data.Type.Natural |
| plusNeutralR | Data.Type.Natural |
| plusStrictMonotone | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| plusSuccL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusSuccR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusZeroL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| plusZeroR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| PNum | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural.Builtin |
| POrd | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural.Builtin |
| predSucc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| predUnique | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| propToBoolLeq | Data.Type.Natural |
| propToClassLeq | Data.Type.Natural |
| Proxy | |
| 1 (Data Constructor) | Data.Type.Natural |
| 2 (Type/Class) | Data.Type.Natural |