| Max | Data.Type.Natural |
| max | Data.Type.Natural |
| maxComm | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| maxLeast | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| maxLeqL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| maxLeqR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| MaxSym0 | Data.Type.Natural |
| MaxSym1 | Data.Type.Natural |
| MaxSym2 | Data.Type.Natural |
| maxZeroL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| maxZeroR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| Min | Data.Type.Natural |
| min | Data.Type.Natural |
| minComm | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| minLargest | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| minLeqL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| minLeqR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| minPlusTruncMinus | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
| MinSym0 | Data.Type.Natural |
| MinSym1 | Data.Type.Natural |
| MinSym2 | Data.Type.Natural |
| minusCong | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
| minusCongL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
| minusCongR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
| minusNilpotent | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| minusPlus | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| minusSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| minusZero | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| minZeroL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| minZeroR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| mkOrdinalQQ | Data.Type.Ordinal |
| mkSNatQQ | Data.Type.Natural.Class |
| multAssoc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multComm | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multCong | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
| multCongL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
| multCongR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
| multEqCancelL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multEqCancelR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multEqSuccElimL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multEqSuccElimR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multOneL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multOneR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multPlusDistrib | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multSuccL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multSuccR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multZeroL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
| multZeroR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |