Stream: Coq users

Topic: alternate

view this post on Zulip zohaze (Dec 10 2022 at 17:27):

Output of (f a b) is bool.When i apply destruct command on if (f a b) then Coq consider it true and then false with
no hypothesis . What command i should apply that in hypothesis it appears as (f a b) =true and
next (f a b) =false also.

view this post on Zulip Johannes Hostert (Dec 10 2022 at 17:30):

destruct (f a b) eqn:Heq will give you Heq : f a b = true or = false additionally.

view this post on Zulip zohaze (Dec 10 2022 at 17:33):

thanks

Last updated: Oct 04 2023 at 23:01 UTC