The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

The problem is that the decision procedure is recursive, in a 
non-trivial way. The following code solves the problem :

Definition test_dec:forall (a1 b1 : test) ,{a1 = b1} + {a1 <> b1}.
fix 1.
repeat decide equality.
Defined.

Le 05/12/2012 13:19, Liang Dou a écrit :
> hi,all
> I have a question when defining the inductive type:
>
> Inductive test : Set:=
> |base : string -> test
> |rule : string -> list test -> test.
>
> When i write the following definition for this inductive type:
>
> Definition test_dec:forall (a1 b1 : test) ,{a1 = b1} + {a1 <> b1}.
>      repeat decide equality.
> Defined.
>
> It doesn't work and seems to go into an infinite loop.
> Then how can i judge if two elements of type "test" are equal?
>
> Thanks!
>
> Lisa