natural-arithmetic-0.1.2.0: Arithmetic of natural numbers

Index

:=:Arithmetic.Unsafe, Arithmetic.Types
<Arithmetic.Unsafe, Arithmetic.Types
<=Arithmetic.Unsafe, Arithmetic.Types
<=?Arithmetic.Nat
<?Arithmetic.Nat
=?Arithmetic.Nat
absurd 
1 (Function)Arithmetic.Lt
2 (Function)Arithmetic.Fin
ascendArithmetic.Fin
ascend'Arithmetic.Fin
ascendingArithmetic.Fin
ascendingSliceArithmetic.Fin
ascendMArithmetic.Fin
ascendM_Arithmetic.Fin
associativeArithmetic.Plus
commutativeArithmetic.Plus
constant 
1 (Function)Arithmetic.Nat
2 (Function)Arithmetic.Lte
3 (Function)Arithmetic.Lt
decrementLArithmetic.Lte
decrementRArithmetic.Lte
demote 
1 (Function)Arithmetic.Nat
2 (Function)Arithmetic.Fin
descendArithmetic.Fin
descend'Arithmetic.Fin
descendingArithmetic.Fin
descendingSliceArithmetic.Fin
descendMArithmetic.Fin
descendM_Arithmetic.Fin
Difference 
1 (Type/Class)Arithmetic.Types
2 (Data Constructor)Arithmetic.Types
EqArithmetic.Unsafe
Fin 
1 (Type/Class)Arithmetic.Types
2 (Data Constructor)Arithmetic.Types
fromStrictArithmetic.Lte
getNatArithmetic.Unsafe
incrementL 
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
indexArithmetic.Types
LtArithmetic.Unsafe
LteArithmetic.Unsafe
monusArithmetic.Nat
Nat 
1 (Type/Class)Arithmetic.Unsafe, Arithmetic.Types
2 (Data Constructor)Arithmetic.Unsafe
oneArithmetic.Nat
plus 
1 (Function)Arithmetic.Nat
2 (Function)Arithmetic.Lte
3 (Function)Arithmetic.Lt
plusLArithmetic.Equal
plusRArithmetic.Equal
proofArithmetic.Types
reflexiveArithmetic.Lte
substituteL 
1 (Function)Arithmetic.Lte
2 (Function)Arithmetic.Lt
substituteR 
1 (Function)Arithmetic.Lte
2 (Function)Arithmetic.Lt
succArithmetic.Nat
symmetricArithmetic.Equal
testEqualArithmetic.Nat
testLessThanArithmetic.Nat
testLessThanEqualArithmetic.Nat
testZeroArithmetic.Nat
threeArithmetic.Nat
toLteLArithmetic.Lt
toLteRArithmetic.Lt
transitive 
1 (Function)Arithmetic.Lte
2 (Function)Arithmetic.Lt
transitiveNonstrictLArithmetic.Lt
transitiveNonstrictRArithmetic.Lt
twoArithmetic.Nat
weakenArithmetic.Fin
weakenL 
1 (Function)Arithmetic.Lte
2 (Function)Arithmetic.Lt
3 (Function)Arithmetic.Fin
weakenR 
1 (Function)Arithmetic.Lte
2 (Function)Arithmetic.Lt
3 (Function)Arithmetic.Fin
withArithmetic.Nat
WithNat 
1 (Type/Class)Arithmetic.Types
2 (Data Constructor)Arithmetic.Types
zero 
1 (Function)Arithmetic.Nat
2 (Function)Arithmetic.Lte
3 (Function)Arithmetic.Lt
zeroLArithmetic.Plus
zeroRArithmetic.Plus