Computed fields with implicit parameters

Stream: lean4

[Parth Shastri]

It appears that @[computed_field] currently does not support fields that take the type parameter as an implicit parameter. In addition to forcing the function to have a more cumbersome type, for some reason this also uses well-founded recursion instead of structural recursion.

inductive List₁ (α : Type u)
  | nil
  | cons (x : α) (xs : List₁ α)
with
  @[computed_field]
  length : (α : Type u) → List₁ α → Nat
    | _, .nil => 0
    | _, .cons x xs => xs.length + 1

inductive List₂ (α : Type u)
  | nil
  | cons (x : α) (xs : List₂ α)
with
  @[computed_field]
  length : {α : Type u} → List₂ α → Nat
    | _, .nil => 0
    | _, .cons x xs => xs.length + 1

inductive List₃ (α : Type u)
  | nil
  | cons (x : α) (xs : List₃ α)
with
  @[computed_field]
  length : List₃ α → Nat
    | .nil => 0
    | .cons x xs => xs.length + 1

example : (List₁.cons x xs).length = xs.length + 1 := rfl
example : (List₂.cons x xs).length = xs.length + 1 := rfl
example : (List₃.cons x xs).length = xs.length + 1 := rfl