Pretty-printing and auto-params

Stream: lean4

[Yury G. Kudryashov]

Hi, here is an #mwe:

import Lean

macro "id_tac" : tactic =>
  `(tactic| (first | exact id))

def f (x : ℕ) (g : ℕ → ℕ := by id_tac) := g x = x

example (h : f 3) : f 3 (· + 5) := _

[Yury G. Kudryashov]

Lean shows both assumption and the goal as f 3

[Jeremy Salwen]

You should still be able to see g's value if you hover over the expressions in the lean infoview.

[Yury G. Kudryashov]

But why auto_param arguments should be hidden? Arguments with default values aren't hidden.

[Mario Carneiro]

I think they are being considered as a kind of implicit argument