Zulip Chat Archive

Stream: general

Topic: the H bug (or not a bug)


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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