Zulip Chat Archive

Stream: new members

Topic: Negated proof on else-branch


view this post on Zulip 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?

view this post on Zulip 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: May 13 2021 at 21:12 UTC