turn off type of proof in infoview

Stream: mathlib4

[Kevin Buzzard]

Trying to debug a porting issue, and I would like to get my lean 4 infoview looking as much like the corresponding lean 3 infoview as possible, because I have super-unwieldy goals. Seems that lean 4 goal view displays the types of proofs by default:

import Mathlib.Tactic

def foo (n : Nat) (hn : n = 37) : ℕ := n

example : foo 37 rfl = 0 := by
  sorry -- ⊢ foo 37 (_ : 37 = 37) = 0

Can I somehow get rid of that : 37 = 37) with some set_option or something? (I can see some good sides to this being the default option, it's just not good for me here)

[Mario Carneiro]

pp.proofs maybe?

[Mario Carneiro]

pp.proofs.withType

[Kevin Buzzard]

Yeah, proofs doesn't do it (one option shows the type, the other one the term :-) ) but set_option pp.proofs.withType false is what I was looking for. Thanks!

[Sebastian Ullrich]

Would withType false be a more reasonable default for widget-enabled infoviews? The option likely is older than widget support.

[Eric Wieser]

Is it possible (and easy) to write delaborators that turn on withType true for just one argument in a function?

[Alex J. Best]

Sebastian Ullrich said:

Would withType false be a more reasonable default for widget-enabled infoviews? The option likely is older than widget support.

I quite like it being on by default, personally. Though sometimes it is irrelevant it is useful information to orient oneself without having to click things

[Kevin Buzzard]

Oh, interestingly I've just run into a situation where it's the other way around. Lean 3 goal

colimit.ι ((category_of_elements.π X).left_op ⋙ A) J ≫
  (adjunction.left_adjoint_of_equiv
    (λ (P : Cᵒᵖ ⥤ Type u₁) (E : ℰ),
      ({hom := ...

Lean 4 goal:

⊢ colimit.ι ((CategoryOfElements.π X).leftOp ⋙ A) J ≫
    (Adjunction.leftAdjointOfEquiv
          (fun P E =>

with no indication of the types of P or E. I've managed to solve my original problem now, but to get displays to match completely one would have to make Lean 4 display the types.