The Coq mailing list

[Liang Dou <ldou.ecnu AT gmail.com>]

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