Stream: Coq users

Topic: add conditions

view this post on Zulip pianke (Apr 15 2023 at 11:05):

if (f a b) then
) else false

(f2 x y) has bool output. Want to add condition (f a b=?true )&& (f2 x y=? false)
insead of (f a b).Want to full fill both to move ahead . Now it always gives false. I should replace && with /\. How i could do it?

view this post on Zulip Pierre Castéran (Apr 15 2023 at 12:37):

Just if f a b && negb(f2 x y) then ... else ... ?

Last updated: Jun 24 2024 at 13:02 UTC