Johan Commelin (Sep 09 2020 at 08:17):
Currently, if you write
variables (p : nat) [hp : fact p.prime]
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?
Last updated: May 15 2021 at 02:11 UTC