Zulip Chat Archive

Stream: new members

Topic: Negated proof on else-branch


Marcus Rossel (Feb 24 2021 at 20:27):

If-then-else expressions give us the option of obtaining a proof of the condition we're checking on the then-branch:

if h : my_condition
then use_condition h
else ...

Is there a way of obtaining a proof of ¬h on the else-branch?

Alex J. Best (Feb 24 2021 at 20:29):

In the else branch the identifier h should refer to a term of type ¬my_condition


Last updated: Dec 20 2023 at 11:08 UTC