The Coq mailing list

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

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.