natural-arithmetic-0.1.2.0: Arithmetic of natural numbers (Index)

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
ascend	Arithmetic.Fin
ascend'	Arithmetic.Fin
ascending	Arithmetic.Fin
ascendingSlice	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
decrementL	Arithmetic.Lte
decrementR	Arithmetic.Lte
demote
1 (Function)	Arithmetic.Nat
2 (Function)	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
Eq	Arithmetic.Unsafe
Fin
1 (Type/Class)	Arithmetic.Types
2 (Data Constructor)	Arithmetic.Types
fromStrict	Arithmetic.Lte
getNat	Arithmetic.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
index	Arithmetic.Types
Lt	Arithmetic.Unsafe
Lte	Arithmetic.Unsafe
monus	Arithmetic.Nat
Nat
1 (Type/Class)	Arithmetic.Unsafe, Arithmetic.Types
2 (Data Constructor)	Arithmetic.Unsafe
one	Arithmetic.Nat
plus
1 (Function)	Arithmetic.Nat
2 (Function)	Arithmetic.Lte
3 (Function)	Arithmetic.Lt
plusL	Arithmetic.Equal
plusR	Arithmetic.Equal
proof	Arithmetic.Types
reflexive	Arithmetic.Lte
substituteL
1 (Function)	Arithmetic.Lte
2 (Function)	Arithmetic.Lt
substituteR
1 (Function)	Arithmetic.Lte
2 (Function)	Arithmetic.Lt
succ	Arithmetic.Nat
symmetric	Arithmetic.Equal
testEqual	Arithmetic.Nat
testLessThan	Arithmetic.Nat
testLessThanEqual	Arithmetic.Nat
testZero	Arithmetic.Nat
three	Arithmetic.Nat
toLteL	Arithmetic.Lt
toLteR	Arithmetic.Lt
transitive
1 (Function)	Arithmetic.Lte
2 (Function)	Arithmetic.Lt
transitiveNonstrictL	Arithmetic.Lt
transitiveNonstrictR	Arithmetic.Lt
two	Arithmetic.Nat
weaken	Arithmetic.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
with	Arithmetic.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
zeroL	Arithmetic.Plus
zeroR	Arithmetic.Plus