| :=: | Arithmetic.Unsafe, Arithmetic.Types |
| :=:# | Arithmetic.Unsafe, Arithmetic.Types |
| < | Arithmetic.Unsafe, Arithmetic.Types |
| <# | Arithmetic.Unsafe, Arithmetic.Types |
| <= | Arithmetic.Unsafe, Arithmetic.Types |
| <=# | Arithmetic.Unsafe, Arithmetic.Types |
| <=? | Arithmetic.Nat |
| <? | Arithmetic.Nat |
| <?# | Arithmetic.Nat |
| =? | Arithmetic.Nat |
| absurd | |
| 1 (Function) | Arithmetic.Lt |
| 2 (Function) | Arithmetic.Fin |
| ascend | Arithmetic.Fin |
| ascend' | Arithmetic.Fin |
| ascendFrom' | Arithmetic.Fin |
| ascendFrom'# | Arithmetic.Fin |
| ascending | Arithmetic.Fin |
| ascendingSlice | Arithmetic.Fin |
| ascendM | Arithmetic.Fin |
| ascendM# | Arithmetic.Fin |
| ascendM_ | Arithmetic.Fin |
| ascendM_# | Arithmetic.Fin |
| associative | Arithmetic.Plus |
| commutative | Arithmetic.Plus |
| constant | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Lte |
| 3 (Function) | Arithmetic.Lt |
| constant# | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Lt |
| construct# | Arithmetic.Fin |
| decrementL | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| decrementL# | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| decrementR | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| decrementR# | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| demote | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Fin |
| demote# | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Fin |
| descend | Arithmetic.Fin |
| descend# | Arithmetic.Fin |
| descend' | Arithmetic.Fin |
| descending | Arithmetic.Fin |
| descendingSlice | Arithmetic.Fin |
| descendM | Arithmetic.Fin |
| descendM_ | Arithmetic.Fin |
| Difference | |
| 1 (Type/Class) | Arithmetic.Types |
| 2 (Data Constructor) | Arithmetic.Types |
| divide | Arithmetic.Nat |
| divideRoundingUp | Arithmetic.Nat |
| Eq | Arithmetic.Unsafe |
| Eq# | Arithmetic.Unsafe |
| Fin | |
| 1 (Type/Class) | Arithmetic.Types |
| 2 (Data Constructor) | Arithmetic.Types |
| Fin# | |
| 1 (Type/Class) | Arithmetic.Unsafe, Arithmetic.Types |
| 2 (Data Constructor) | Arithmetic.Unsafe |
| Fin32# | |
| 1 (Type/Class) | Arithmetic.Unsafe, Arithmetic.Types |
| 2 (Data Constructor) | Arithmetic.Unsafe |
| fromInt | Arithmetic.Fin |
| fromInt# | Arithmetic.Fin |
| fromStrict | Arithmetic.Lte |
| fromStrict# | Arithmetic.Lte |
| fromStrictSucc | Arithmetic.Lte |
| fromStrictSucc# | Arithmetic.Lte |
| getNat | Arithmetic.Unsafe |
| incrementL | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| 3 (Function) | Arithmetic.Fin |
| incrementL# | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| incrementR | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| 3 (Function) | Arithmetic.Fin |
| incrementR# | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| 3 (Function) | Arithmetic.Fin |
| index | Arithmetic.Types |
| lift | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Lte |
| 3 (Function) | Arithmetic.Lt |
| 4 (Function) | Arithmetic.Equal |
| 5 (Function) | Arithmetic.Fin |
| Lt | Arithmetic.Unsafe |
| Lt# | Arithmetic.Unsafe |
| Lte | Arithmetic.Unsafe |
| Lte# | Arithmetic.Unsafe |
| MaybeFin# | |
| 1 (Type/Class) | Arithmetic.Unsafe, Arithmetic.Types |
| 2 (Data Constructor) | Arithmetic.Unsafe |
| MaybeFinJust# | Arithmetic.Types |
| MaybeFinNothing# | Arithmetic.Types |
| monus | Arithmetic.Nat |
| N0# | Arithmetic.Nat |
| N1# | Arithmetic.Nat |
| N1024# | Arithmetic.Nat |
| N128# | Arithmetic.Nat |
| N16# | Arithmetic.Nat |
| N2# | Arithmetic.Nat |
| N2048# | Arithmetic.Nat |
| N256# | Arithmetic.Nat |
| N3# | Arithmetic.Nat |
| N32# | Arithmetic.Nat |
| N4# | Arithmetic.Nat |
| N4096# | Arithmetic.Nat |
| N5# | Arithmetic.Nat |
| N512# | Arithmetic.Nat |
| N6# | Arithmetic.Nat |
| N64# | Arithmetic.Nat |
| N7# | Arithmetic.Nat |
| N8# | Arithmetic.Nat |
| Nat | |
| 1 (Type/Class) | Arithmetic.Unsafe, Arithmetic.Types |
| 2 (Data Constructor) | Arithmetic.Unsafe |
| Nat# | |
| 1 (Type/Class) | Arithmetic.Unsafe, Arithmetic.Types |
| 2 (Data Constructor) | Arithmetic.Unsafe |
| one | Arithmetic.Nat |
| one# | Arithmetic.Nat |
| plus | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Lte |
| 3 (Function) | Arithmetic.Lt |
| plus# | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Lte |
| 3 (Function) | Arithmetic.Lt |
| plusL | Arithmetic.Equal |
| plusL# | Arithmetic.Equal |
| plusR | Arithmetic.Equal |
| plusR# | Arithmetic.Equal |
| proof | Arithmetic.Types |
| reciprocalA | Arithmetic.Lt |
| reciprocalB | Arithmetic.Lt |
| reflexive | Arithmetic.Lte |
| reflexive# | Arithmetic.Lte |
| remInt# | Arithmetic.Fin |
| remWord# | Arithmetic.Fin |
| substituteL | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| substituteR | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| succ | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Fin |
| succ# | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Fin |
| symmetric | Arithmetic.Equal |
| testEqual | Arithmetic.Nat |
| testEqual# | Arithmetic.Nat |
| testLessThan | Arithmetic.Nat |
| testLessThan# | Arithmetic.Nat |
| testLessThanEqual | Arithmetic.Nat |
| testZero | Arithmetic.Nat |
| testZero# | Arithmetic.Nat |
| three | Arithmetic.Nat |
| times | Arithmetic.Nat |
| toLteL | Arithmetic.Lt |
| toLteR | Arithmetic.Lt |
| transitive | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| transitive# | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| transitiveNonstrictL | Arithmetic.Lt |
| transitiveNonstrictL# | Arithmetic.Lt |
| transitiveNonstrictR | Arithmetic.Lt |
| transitiveNonstrictR# | Arithmetic.Lt |
| two | Arithmetic.Nat |
| unlift | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Lte |
| 3 (Function) | Arithmetic.Lt |
| 4 (Function) | Arithmetic.Fin |
| weaken | Arithmetic.Fin |
| weakenL | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| 3 (Function) | Arithmetic.Fin |
| weakenL# | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| weakenLhsL# | Arithmetic.Lt |
| weakenLhsR# | Arithmetic.Lt |
| weakenR | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| 3 (Function) | Arithmetic.Fin |
| weakenR# | |
| 1 (Function) | Arithmetic.Lte |
| 2 (Function) | Arithmetic.Lt |
| with | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Fin |
| with# | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Fin |
| WithNat | |
| 1 (Type/Class) | Arithmetic.Types |
| 2 (Data Constructor) | Arithmetic.Types |
| zero | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Lte |
| 3 (Function) | Arithmetic.Lt |
| zero# | |
| 1 (Function) | Arithmetic.Nat |
| 2 (Function) | Arithmetic.Lt |
| zeroL | Arithmetic.Plus |
| zeroR | Arithmetic.Plus |