Zulip Chat Archive

Stream: new members

Topic: type of `not`

view this post on Zulip Scott Olson (Oct 08 2018 at 22:55):

Is there a reason we have def not : Prop → Prop rather than def not : Sort u → Prop?

I had some proofs of ¬foo which I had to change to foo → false when I changed foo from a simple Prop to a structure sigma Type, but it seems like it would make sense to still say ¬foo.

view this post on Zulip Simon Hudon (Oct 08 2018 at 23:03):

It's probably a matter of convention. ¬p, you usually assume that p is a proposition . An operation such as you describe might more usefully be called is_empty

view this post on Zulip Mario Carneiro (Oct 08 2018 at 23:30):

there used to be a ~A notation for this, but it didn't get used enough to be worth it.

Last updated: May 10 2021 at 19:16 UTC