Zulip Chat Archive

Stream: general

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 in var > 0 or var \in s, and use hvar.

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: Aug 03 2023 at 10:10 UTC