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
Last updated: May 13 2021 at 21:12 UTC