Stream: Coq users

Topic: apply destruct

view this post on Zulip pianke (Feb 09 2023 at 15:17):

I have a function with two arguments f(a b) , while f checks the equality of a and b.First time it consider it true next false.But i want to make it visible in hypothesis like H:a=b next a<>b .(I have applied destruct as H ,but get this message "Disjunctive/conjunctive introduction pattern expected."

view this post on Zulip Pierre Castéran (Feb 09 2023 at 16:00):

In the following context:

Variables (A: Type)(f : forall a b:A, {a = b}+{a <> b}).

You may try destruct (f a b) as [Heq | Hneq].

Last updated: Oct 04 2023 at 23:01 UTC