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 |