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

Stream: mathlib4

[Arien Malec]

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]

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]

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

[Arien Malec]

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

[Yury G. Kudryashov]

I failed to find Logic.Equiv.ULift.

[Yury G. Kudryashov]

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

[Arien Malec]

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

[Arien Malec]

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

[Yury G. Kudryashov]

(deleted)