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.
Return 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
Convert an 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 Fin Z
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