Fin

structure Fin[n: Nat] {
    value: Nat
} constraint {
    value < n
}

Finite initial segment { 0, 1, ..., n - 1 }.

GitHub

---

again

define again(self) -> Fin[n] {
    fin_self(n, self)
}

Rewrap through a top-level dependent satisfy function.

bound

define bound(self) -> Nat {
    n
}

Expose the ambient bound in a family-dependent attribute body.

value

Fin.value: Fin[x0] -> Nat