The Coq mailing list

[Djamila Baroudi <baroudi.d7 AT gmail.com>]

hello, you mean that i should write for example this:

 Inductive st :Set:= q0 | q1 |q2 .
>>     Inductive acts:Set:=pred(p:nat)|event(e:bool).
>>     Definition a :acts:=pred(1).
>>     Definition b:acts:=pred(2).
>>     Definition c:acts:=event(true).
>>     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.

but with this code i have always a same error.

thanks for your informations.

2014-03-18 10:54 GMT+01:00 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.
>>
>>

--

Mlle Djamila Baroudi                           

Faculté des Sciences Exactes et Informatique,        

Université de Mostaganem,

27000 Mostaganem, Algérie.