Zulip Chat Archive

Stream: general

Topic: include

Johan Commelin (Sep 09 2020 at 08:17):

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?

Last updated: Aug 03 2023 at 10:10 UTC