Zulip Chat Archive

Stream: lean4

Topic: Prop Def?


view this post on Zulip Mac (Mar 11 2021 at 16:52):

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

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

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

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

view this post on Zulip 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: May 18 2021 at 23:14 UTC