match-syntax leftovers

[leodemoura]

The auxiliary variables created by match-syntax expander are visible in the infoview.
It does not bother the developers too much because most of us use Emacs, but during the ICERM after-party hackton, it was an issue for people using VS Code.
Example:

[digama0]

Suggestion: clear% x y in e term mode syntax for clear as part of the generated code for the quotation. (% because I don't know if clear being a keyword will cause problems.) Alternatively, a let_fun with the match body can be introduced before all the lets are created (not sure if this affects the performance).

[Kha]

The auxiliary variables are shown here only because of forward dependencies from the let-bound pattern variables. I think the more fundamental question is, should we even show the value of let-bound variables at all in programming contexts? I'm pretty sure no other programming language does that at least. Not sure if hiding them based on the Prop-ness of the goal would be confusing when switching between prop and data contexts within the same definition (however, that is already true for the current hiding logic of inaccessibles). If that seems likely, a compromise could be to only hide let values that contain inaccessibles in non-prop contexts, as these were certainly not written down by the user at least.

[gebner]

I think the more fundamental question is, should we even show the value of let-bound variables at all in programming contexts?

I think we should absolutely show let-values, because they are just as important as types. For example, let_fun n := 42; (.ofNat 0 : Fin n) doesn't type-check but let n := 42; (.ofNat 0 : Fin n) does. (And this is essentially what the term goal display should answer: what do I need to construct here, what will type check here?)

There is an argument to be made to (maybe) collapse (large) let-values by default (à la leanprover/vscode-lean4#76 (comment)), but there should definitely be an indication that this is a let-binding, and the let-value should be inspectable in the infoview.

I'm pretty sure no other programming language does that at least.

Most other programming languages don't have ζ-reduction (on the type level), so the let-value doesn't make a difference for type-checking. And most don't show the local context at all.

switching between prop and data contexts

Note that Prop is an extremely flaky heuristic: there's lots of stuff in Type that behaves like a proposition. For example, bundled isomorphisms serve a similar purpose as equalities (we even have a rewrite tactic for them in mathlib). It's confusing when they are hidden differently.

[digama0]

Another idea might be to somehow discourage the use of let bound variables entirely in programming contexts. I think that it is very rare to actually need a dependent let, but the current situation encourages using let way more than required. The best mechanism I can think of is to rename let to let dep or def or something and make let in do blocks and possibly elsewhere mean have instead.

[Kha]

It's a bit like in the module system: perhaps reducibility is not the right default after all, in all cases.

[leodemoura]

Another idea might be to somehow discourage the use of let bound variables entirely in programming contexts. I think that it is very rare to actually need a dependent let, but the current situation encourages using let way more than required. The best mechanism I can think of is to rename let to let dep or def or something and make let in do blocks and possibly elsewhere mean have instead.

I think this is a good change.

I agree we rarely need dependent let in programming contexts, the main exception is local instances.