The Coq mailing list

[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