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

natural-arithmetic-0.1.4.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
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
construct#	Arithmetic.Fin
decrementL
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
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
Fin
1 (Type/Class)	Arithmetic.Types
2 (Data Constructor)	Arithmetic.Types
Fin#
1 (Type/Class)	Arithmetic.Unsafe, Arithmetic.Types
2 (Data Constructor)	Arithmetic.Unsafe
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
lift
1 (Function)	Arithmetic.Nat
2 (Function)	Arithmetic.Fin
Lt	Arithmetic.Unsafe
Lte	Arithmetic.Unsafe
monus	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
plus
1 (Function)	Arithmetic.Nat
2 (Function)	Arithmetic.Lte
3 (Function)	Arithmetic.Lt
plus#	Arithmetic.Nat
plusL	Arithmetic.Equal
plusR	Arithmetic.Equal
proof	Arithmetic.Types
reciprocalA	Arithmetic.Lt
reciprocalB	Arithmetic.Lt
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
times	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
unlift
1 (Function)	Arithmetic.Nat
2 (Function)	Arithmetic.Fin
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
1 (Function)	Arithmetic.Nat
2 (Function)	Arithmetic.Fin
with#	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#	Arithmetic.Nat
zeroL	Arithmetic.Plus
zeroR	Arithmetic.Plus