Sort is Prop

Stream: general

[Yaël Dillies]

Just as Type refers to Type 0, Sort refers to Sort 0, aka Prop. Given that we already have this Prop spelling, wouldn't it be better if Sort meant the same as Sort*?

[Kevin Buzzard]

It's certainly occasionally tripped up people in the past

[Eric Wieser]

Or just have it be illegal without the * or universe

[Adam Topaz]

I think this suggestion would confuse me more!
I would suggest simply disallowing Sort

[Kevin Buzzard]

I presume Adam means Yael's suggestion. I think removing Sort is a great idea. I bet you never see bare sort in the docs either, except for that one line when they explain that it means Prop.

[Junyan Xu]

Fun fact: Prop is a notation not a definition and therefore doesn't show up in the docs.

[Kyle Miller]

I think this is where unadorned Sort gets parsed: https://github.com/leanprover-community/lean/blob/bfce34363b0efe86e93e3fe75de76ab3740c772d/src/frontends/lean/builtin_exprs.cpp#L101

[Kyle Miller]

But reading the code, I'm not exactly sure how Sort u works. It only seems to have Sort.{u} here.

[Adam Topaz]

Kevin Buzzard said:

I presume Adam means Yael's suggestion. I think removing Sort is a great idea. I bet you never see bare sort in the docs either, except for that one line when they explain that it means Prop.

Yes, that's what I meant... Eric's comment came in as I was pressing enter ;)

[Stuart Presnell]

Kevin Buzzard said:

I bet you never see bare sort in the docs either, except for that one line when they explain that it means Prop.

A (case-sensitive) search of mathlib turns up 1083 instances of the string Sort, all of which are either Sort*, Sort u (for some expression u) or in comments. I can't find a single use of unadorned Sort in mathlib code.

[Mario Carneiro]

lean#732. It doesn't show up even once in the entire lean core library + test suite either

[Mario Carneiro]

@Kyle Miller The way the parsing works is that when it reads Sort it creates a syntax like sort_wo_universe(Sort 0), and then later if it sees a level parameter following this it will strip the sort_wo_universe annotation producing Sort l. (This way, Sort 0 0 does not spuriously get accepted.) The fix implemented above does not try to catch this at parse time and instead refuses to elaborate sort_wo_universe(Sort 0) to Prop

[Yaël Dillies]

Thanks Mario!