Zulip Chat Archive

Stream: lean4

Topic: Prop Def?


Mac (Mar 11 2021 at 16:52):

Why is Prop a keyword and not just a definition? I.e., def Prop := Sort 0

Mario Carneiro (Mar 11 2021 at 16:58):

It has to at least be a notation, because lots of stuff assumes that universes are of the form Sort u

Mario Carneiro (Mar 11 2021 at 16:58):

It was a notation in lean 3, but it was turned into a keyword in lean 4 and I'm not sure what the reason is

Sebastian Ullrich (Mar 11 2021 at 17:06):

Notations also introduce keywords. It is built-in syntax because user-defined syntax was implemented way later.

Mac (Mar 11 2021 at 17:17):

Sebastian Ullrich said:

It is built-in syntax because user-defined syntax was implemented way later.

Okay, but now that user-defined syntax does exist, wouldn't it make sense to make it notation now?


Last updated: Dec 20 2023 at 11:08 UTC