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