include

Stream: general

[Johan Commelin]

Currently, if you write

variables (p : nat) [hp : fact p.prime]

then hp will not be auto-included in all lemmas that mention p. On the other hand, having this variable names is really convenient, because you can then write hp.pos for the proof that 0 < p. Whereas referring to some _inst_1 is evil and ugly.

How hard would it be to change Lean so that it also auto-includes explicitly named instance variables?