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

[Floris van Doorn]

I am often annoyed by this behavior, since clicking around in the infoview is an extra step that has to be performed very often.
I made a Lean issue: lean4#3548. If you agree, please upvote.

[Kyle Miller]

I fixed this in lean4#3375, and you can expect it in the next Lean release :smile:

[Floris van Doorn]

oh yay! That was quick :tada:

[Patrick Massot]

I knew I was missing a trick for efficient Lean dev. It was time travel.