Zulip Chat Archive

Stream: mathlib4

Topic: Naming for `forall`/`exists` as theorem names


Arien Malec (Nov 24 2022 at 03:58):

forall isn't a legal Lean name (as a reserved word_, but exists as theorem names in mathlib

I noted that, following upstream mathlib, in Data.ULift the name is «forall», and in Logic.Equiv.ULift the name is forall₃ (both are apparently referenced as foreall

It's weird that there are two ways of doing this....

Jireh Loreaux (Nov 24 2022 at 04:01):

forall is special because it's ASCII for . The «forall» syntax allows you to use it as a name anyway; here «» is a special kind of quote that allows you to use symbols not normally allowed in declaration names.

Jireh Loreaux (Nov 24 2022 at 04:02):

But we don't include the quotes when we refer to them in theorems.

Arien Malec (Nov 24 2022 at 04:05):

I think I get that - but note that Logic.Equiv.ULift does it differently....

Yury G. Kudryashov (Nov 26 2022 at 16:55):

I failed to find Logic.Equiv.ULift.

Yury G. Kudryashov (Nov 26 2022 at 16:56):

Which file are you talking about? Data.ULift defines ULift.forall etc using «».

Arien Malec (Nov 26 2022 at 17:24):

I may have hallucinated the existence? I can't find it anymore...

Arien Malec (Nov 26 2022 at 17:31):

Perhaps was confused by the "Multi-airity" flavors of forall/exist that are in Function.Surjective

Yury G. Kudryashov (Nov 26 2022 at 18:33):

(deleted)


Last updated: Dec 20 2023 at 11:08 UTC