Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] This clause is redundant error

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] This clause is redundant error


Chronological Thread 
  • From: Beta Ziliani <beta AT mpi-sws.org>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] This clause is redundant error
  • Date: Tue, 18 Mar 2014 10:52:44 +0100

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.
>
>



Archive powered by MHonArc 2.6.18.

Top of Page