English
ofNatCode decodes a natural into a Code; it defines 0 → zero, 1 → succ, 2 → left, 3 → right, and for n+4 uses a nested unpair structure to decide whether to form pair, comp, prec, or rfind'.
Русский
ofNatCode декодирует число в Code; 0→zero, 1→succ, 2→left, 3→right, а для n+4 далее через разбор m = n.div2.div2 с помощью unpair определяет, строит ли pair, comp, prec или rfind'.
LaTeX
$$$\\operatorname{ofNatCode} : \\mathbb{N} \\to \\text{Code}, \\quad 0 \\mapsto \\mathrm{zero}, 1 \\mapsto \\mathrm{succ}, 2 \\mapsto \\mathrm{left}, 3 \\mapsto \\mathrm{right}, \\text{and } n+4 \\mapsto \\text{(via } m = n.div2.div2 ext{ and unpair) pair/comp/prec/rfind' }$$$
Lean4
/-- A decoder for `Nat.Partrec.Code.encodeCode`, taking any ℕ to the `Nat.Partrec.Code` it represents.
-/
def ofNatCode : ℕ → Code
| 0 => zero
| 1 => succ
| 2 => left
| 3 => right
| n + 4 =>
let m := n.div2.div2
have hm : m < n + 4 := by
simp only [m, div2_val]
exact
lt_of_le_of_lt (le_trans (Nat.div_le_self _ _) (Nat.div_le_self _ _)) (Nat.succ_le_succ (Nat.le_add_right _ _))
have _m1 : m.unpair.1 < n + 4 := lt_of_le_of_lt m.unpair_left_le hm
have _m2 : m.unpair.2 < n + 4 := lt_of_le_of_lt m.unpair_right_le hm
match n.bodd, n.div2.bodd with
| false, false => pair (ofNatCode m.unpair.1) (ofNatCode m.unpair.2)
| false, true => comp (ofNatCode m.unpair.1) (ofNatCode m.unpair.2)
| true, false => prec (ofNatCode m.unpair.1) (ofNatCode m.unpair.2)
| true, true => rfind' (ofNatCode m)
