Unexpander for function composition

Stream: lean4

[Dan Velleman]

Try this:

example (f g : Nat → Nat) : f ∘ f = g := by
  done

example (f g : Nat → Nat) : (f ∘ f) 0 = g 0 := by
  done

In the first example, the goal in the tactic state is f ∘ f = g, as it should be. In the second example, the goal in the tactic state is Function.comp f f 0 = g 0. I think we need something like:

@[app_unexpander Function.comp] def unexpandFunctionComp : Lean.PrettyPrinter.Unexpander
  | `($(_) $f:term $g:term $x:term) => `(($f ∘ $g) $x)
  | _ => throw ()