English
Using type-class inference to construct Fin2 n from a Nat m when m < n, i.e., a canonical bound-based embedding.
Русский
Используется вывод типов, чтобы получить Fin2 n из натурального m, если m < n — каноническое вложение по границе.
LaTeX
$$$\text{ofNat'} : ∀{n}, m \to [IsLT m n] \to Fin2 n$$$
Lean4
/-- Use type class inference to infer the boundedness proof, so that we can directly convert a
`Nat` into a `Fin2 n`. This supports notation like `&1 : Fin 3`. -/
def ofNat' : ∀ {n} (m) [IsLT m n], Fin2 n
| 0, _, h => absurd h.h (Nat.not_lt_zero _)
| succ _, 0, _ => fz
| succ n, succ m, h => fs (@ofNat' n m ⟨lt_of_succ_lt_succ h.h⟩)
