reserved words

Stream: new members

[Patrick Thomas]

Is there a way to have forall as a constructor, by requiring it to be used as formula.forall or something similar?

inductive formula : Type
| false : formula
| true : formula
| var : string → formula
| not : formula → formula
| and : formula → formula → formula
| or : formula → formula → formula
| imp : formula → formula → formula
| iff : formula → formula → formula
| forall : string → formula → formula
| exists : string → formula → formula

[Yaël Dillies]

Write it «forall», with \f<< and \f>>

[Yaël Dillies]

You'll probably have to write «exists»as well.

[Patrick Thomas]

Thank you!

[Eric Wieser]

Or \f<<>> which will type both at once

[Yaël Dillies]

Oh, didn't know about that one!

[Patrick Thomas]

What does this syntax mean? Is it just for this purpose or something more general?

[Kyle Miller]

It's the quotation notation for names in Lean. It lets you use characters that aren't permitted for unquoted names:

namespace «zulip people»

def «Patrick Thomas» : string := "that is Patrick's name"

end «zulip people»

#eval «zulip people».«Patrick Thomas»

[Patrick Thomas]

I see. Thank you.