Topic: the H bug (or not a bug)
Yury G. Kudryashov (Mar 29 2021 at 04:23):
Currently expressions like
⋃ x ∈ s, f x add
(H : x ∈ s) to the context. Manifolds use
H as a variable name for the model space, and this creates conflicts similar to the
a bug. Should we use the same strange symbol for
(_ : x ∈ s) or ban
H as a variable name?
Johan Commelin (Mar 29 2021 at 04:52):
It would be great if Lean would look at the name of the variable
var > 0 or
var \in s, and use
Johan Commelin (Mar 29 2021 at 04:53):
I think that's a predictable rule that will avoid 99.5% of all conflicts.
Last updated: May 08 2021 at 18:17 UTC