Adrián García (May 08 2021 at 19:59): Adrián García (May 08 2021 at 19:59):Hi, I'im trying to prove the equality for an slist of inductive types, but I cannot prove it unless I know that X is decidable, but how can I tell to Coq that X is decidable in eq_dec_slist proposition?
Inductive slist (X: Type): Type :=
| empty : slist X
| snoc : slist X -> X -> slist X.
Arguments empty {X}.
Arguments snoc {X} _ _.
Proposition eq_dec_slist (X: Type) (G G': slist X): {G = G'} + {G <> G'}.
Proof.
intros.
decide equality.
Abort.
you should add it as an hypothesis:
Proposition eq_dec_slist (X: Type) (deceqX : forall x x' : X, {x = x'} + {x <> x'}) (G G': slist X): {G = G'} + {G <> G'}.
Proof.
intros.
decide equality.
Defined.
Last updated: Oct 13 2024 at 01:02 UTC