Lean4 infoview formatting

Stream: new members

[Kevin Sullivan]

Late to the game, I'm moving to Lean 4. I will have some dumb questions. Here are a few

#check Nat. add produces this output in the infoview: Nat.add (a:cross:a:cross:¹ : Nat) : Nat.

1. What command should I issue to tell Lean4 to render the type using ordinary arrow notation
2. How should I understand this notation? a:cross:a:cross:¹
3. What does @& mean as in "String → (@& String) → String"
4. Where is this stuff documented?

Thank you!

[Kyle Miller]

1. #check (Nat.add) should do
2. the "tombstones" are a way to make names that the user can't type; it's an improvement on
3. @& is part of the C ABI and you can ignore it if you don't care about the interface between Lean and C. (It indicates that the argument is only borrowed, impacting who's responsible for updating reference counts.)

[Kevin Sullivan]

Kyle Miller said:

1. #check (Nat.add) should do
2. the "tombstones" are a way to make names that the user can't type; it's an improvement on
3. @& is part of the C ABI and you can ignore it if you don't care about the interface between Lean and C. (It indicates that the argument is only borrowed, impacting who's responsible for updating reference counts.)

Thank you. Also useful: https://stackoverflow.com/questions/76655498/output-of-check-nat-add. And borrowing is documented here: https://leanprover.github.io/lean4/doc/dev/ffi.html.

[Robert hackman]

(deleted)

[Kevin Buzzard]

Can you post a #mwe of what you have tried? The best way to ask a question here is by posting fully working code showing where you're stuck

[Robert hackman]

oups sorry wrong topic