Unfolding in structural recursion

Stream: lean4

[Aaron Liu]

What would need to happen for Tree.mapWF to be processed like Tree.map?

/-- The type of ordered finitely branching trees with leaves labeled by `α`. -/
inductive Tree.{u} (α : Type u) where
  | leaf : α → Tree α
  | branch : List (Tree α) → Tree α

-- uses `WellFounded.fix` :(
def Tree.mapWF.{u, v} {α : Type u} {β : Type v} (f : α → β) (t : Tree α) : Tree β :=
  match t with
    | .leaf a => .leaf (f a)
    | .branch xs => .branch (xs.map (mapWF f))

mutual

-- uses `Tree.brecOn`
def Tree.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (t : Tree α) : Tree β :=
  match t with
    | .leaf x => .leaf (f x)
    | .branch xs => .branch (mapList f xs)

-- uses `Tree.brecOn_1`
def Tree.mapList.{u, v} {α : Type u} {β : Type v} (f : α → β) (t : List (Tree α)) : List (Tree β) :=
  match t with
    | [] => []
    | x :: xs => x.map f :: mapList f xs

end