The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hi.

try

Definition PATH_dec : forall x y : ID, {x = y} + {x <> y}.

Proof. repeat decide equality. Defined.

Cheers.

2014-12-10 1:53 GMT+01:00 Saulo Araujo <saulo2 AT gmail.com>:

Hi,

I need to compare values of the type PATH defined below

Definition ID := string.

Inductive STEP : Type := 

  | LastStep : ID -> STEP | Step : ID -> PATH -> STEP | Init : ID -> STEP

with PATH : Type := Path : list STEP -> PATH.

Is there a way to compare those values in Gallina like we compare them in SML?

I tried the suggestion in http://stackoverflow.com/questions/6636131/searching-through-a-list-recursively-in-coq

Definition PATH_dec : forall x y : ID, {x = y} + {x <> y}.

Proof. decide equality. Defined.

but Coq says Error: Attempt to save an incomplete proofCompilation output:

Thanks in advance,

Saulo

--

Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.