Alternative to `#check` that does not show signatures?

Stream: lean4

[David Thrane Christiansen]

Since about two weeks ago (commit de9a6374f182586ad597dc7d720cfc2139f488f3), Lean shows signatures rather than types when #check is directly used on an identifier. For example, given

def add1 (n : Nat) : Nat := n + 1

it used to be the case that #check add1 returned Nat -> Nat, while it now returns add1 (n : Nat) : Nat.

This is great! It makes the whole thing simpler and easier to figure out, and argument names are pretty handy for understanding library code.

However, it leaves me with a conundrum. In Functional Programming in Lean, I've been trying to provide readers with ways that they can empirically check what I'm writing. When explaining the function type, the old behavior of #check was very convenient, as it allowed readers to dash off a quick definition and see the resulting function type, and play with the one and see the changes in the other. This also supported the goal of getting them used to the Lean interactive environment while learning the basics of the language. I can certainly just tell readers what the type is, but I thought I'd ask here if there's some other feature I can easily use for complete beginners to see the type, rather than signature, of a defined name.

Thanks!

[Reid Barton]

I think #check (add1) will give the old behavior--not sure whether that's something you want to recommend...

[David Thrane Christiansen]

The closest I've come is adding a type ascription: #check (add1 : Nat → Nat). It's less fun to experiment with, because it provides feedback in the form of error messages rather than info output and it requires a bit more understanding to be present prior to experimentation, but it mostly does what's wanted here.

[David Thrane Christiansen]

Oooh, the parentheses trick is nice! I think that's a perfectly reasonable thing to do here. Thanks!