coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
>
>
- [Coq-Club] This clause is redundant error, Djamila Baroudi, 03/18/2014
- Re: [Coq-Club] This clause is redundant error, Beta Ziliani, 03/18/2014
- Re: [Coq-Club] This clause is redundant error, Beta Ziliani, 03/18/2014
- Re: [Coq-Club] This clause is redundant error, Djamila Baroudi, 03/18/2014
- Re: [Coq-Club] This clause is redundant error, Beta Ziliani, 03/18/2014
- Re: [Coq-Club] This clause is redundant error, Djamila Baroudi, 03/18/2014
- Re: [Coq-Club] This clause is redundant error, Beta Ziliani, 03/18/2014
- Re: [Coq-Club] This clause is redundant error, Djamila Baroudi, 03/18/2014
- Re: [Coq-Club] This clause is redundant error, Beta Ziliani, 03/18/2014
- Re: [Coq-Club] This clause is redundant error, Beta Ziliani, 03/18/2014
Archive powered by MHonArc 2.6.18.