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
Convert an Integer to a Fin in the required bounds/
This is essentially a composition of
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