Weaken the bound on a Fin by some amount
Weaken the bound on a Fin by 1
Attempt to tighten the bound on a Fin.
Left if the bound could not be tightened, or
Right if it could.
Add some natural number to a Fin, extending the bound accordingly
the previous bound
the number to increase the Fin by
The largest element of some Fin type
Integer to a
Fin, provided the integer is within bounds.
The upper bound of the Fin
Allow overloading of Integer literals for Fin.
the Integer that the user typed
an automatically-constructed proof that
x is in bounds
finToNat is injective
Convert a Fin to a Nat
Convert a Fin to an Integer
There are no elements of
Numbers strictly less than some bound. The name comes from "finite sets".
It's probably not a good idea to use
Fin for arithmetic, and they will be
exceedingly inefficient at run time.
the upper bound
Substract two Fins, keeping the bound of the minuend
Add two Fins, extending the bound
Multiply two Fins, extending the bound