code generator does not support recursor

Stream: new members

[Lars Ericson]

This is a piece of code from a year and a half ago, which assumes an ability to define a function by induction which I am guessing worked at that time:

def rename_all_bound_pf (φ : Form N) (x : SVAR) : ⊢ (φ ⟷ (φ.replace_bound x)) := by
  induction φ with
  | bind z φ ih =>
      rw [Form.replace_bound]
      by_cases h : z = x
      . simp only [h, ite_true]
        sorry
      . simp only [h, ite_false]
        sorry
  | impl φ ψ ih1 ih2 =>
      exact Proof.mp (Proof.mp (Proof.tautology iff_imp) ih1) ih2
  | box φ ih =>
      let l1 := Proof.mp Proof.ax_k (Proof.necess (Proof.mp (Proof.tautology iff_elim_l) ih))
      let l2 := Proof.mp Proof.ax_k (Proof.necess (Proof.mp (Proof.tautology iff_elim_r) ih))
      let l3 := Proof.mp (Proof.mp (Proof.tautology iff_intro) l1) l2
      exact l3
  | _ =>
      sorry

Today it gives me this error message:

code generator does not support recursor 'Form.rec' yet, consider using 'match ... with' and/or structural recursion

Here is a rewrite which passes typecheck as of most recent Lean 4 and uses match instead of induction:

def rename_all_bound_pf (φ : Form N) (x : SVAR) : ⊢ (φ ⟷ (φ.replace_bound x)) :=
  match φ with
  | Form.bind z ψ =>
      have ih := rename_all_bound_pf ψ x
      sorry -- Fill in the proof for this case
  | Form.impl φ₁ φ₂ =>
      have ih1 := rename_all_bound_pf φ₁ x
      have ih2 := rename_all_bound_pf φ₂ x
      Proof.mp (Proof.mp (Proof.tautology iff_imp) ih1) ih2
  | Form.box ψ =>
      have ih := rename_all_bound_pf ψ x
      let l1 := Proof.mp Proof.ax_k (Proof.necess (Proof.mp (Proof.tautology iff_elim_l) ih))
      let l2 := Proof.mp Proof.ax_k (Proof.necess (Proof.mp (Proof.tautology iff_elim_r) ih))
      let l3 := Proof.mp (Proof.mp (Proof.tautology iff_intro) l1) l2
      l3
  | _ =>
      sorry

What is the most Lean-onic way to define this kind of function in current usage which will be supported going forward?