The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Sorry, forgot to mention that Coq is treating a,b,c in each pattern
matching clause as variables, and this is why is giving you the error.

On Tue, Mar 18, 2014 at 10:52 AM, Beta Ziliani 
<beta AT mpi-sws.org>
 wrote:
> Basically your definitions a, b, c of acts are not constructors for
> the inductive type acts, which is what Coq expects (as most languages)
> in the match.  Also, take into account that writing
>
> Definition a : acts.
>
> is opening a goal to fill: what is a?  Probably what you meant is
>
> Axiom a : acts.
>
> (but be careful with axioms!).
>
> Hope it helps,
> Beta
>
>
>
> On Tue, Mar 18, 2014 at 10:42 AM, Djamila Baroudi 
> <baroudi.d7 AT gmail.com>
>  wrote:
>> hello,
>> i have a problem with definition of an automaton, an error was shown when i
>> create this code:
>>
>>
>>     (*automate*)
>>
>>     Record automaton :Type:=
>>     mk_auto {
>>        states : Set;
>>        actions :Set;
>>        initial : states;
>>        transitions : states -> actions -> list states
>>     }.
>>     (*States*)
>>     Inductive st :Set:= q0 | q1 |q2 .
>>     Inductive acts:Set:=pred(p:nat)|event(e:bool).
>>     Definition a :acts.
>>     Definition b:acts.
>>     Definition c:acts.
>>     Function trans (q:st)(x:acts) :list st :=
>>     match q, x with
>>       | q0, a =>  cons q1 nil
>>       | q1, b =>  cons q0 nil
>>       | q1, c =>  cons q2 nil
>>       | _,_ =>    nil (A:=_)
>>     end.
>> the error was:
>> Error: This clause is redundant. (underlined this clause " | q1, c =>  cons
>> q2 nil")
>>
>> Thanks.
>>
>> --
>>
>> Mlle Djamila Baroudi
>>
>> Faculté des Sciences Exactes et Informatique,
>>
>> Université de Mostaganem,
>>
>> 27000 Mostaganem, Algérie.
>>
>>