Stream: new members
Topic: type of `not`
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
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
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