coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frederic Blanqui <frederic.blanqui AT inria.fr>
- To: Coq-Club Club <coq-club AT inria.fr>
- Subject: [Coq-Club] definition accepted by coqc but not accepted by coqtop
- Date: Wed, 10 Oct 2012 16:12:17 +0800
Hello.
I have a problem for having both coqc and coqtop accept some definition:
Section S1.
Variable A : Type.
Inductive t := c : A -> t.
End S1.
Section S2.
Variable A : Type.
Notation c := (c A).
(* this first definition is not accepted because c is a notation:
Definition f (x : t A) := match x with c _ => 0 end.*)
(* this second definition is accepted by coqtop (ProofGeneral) but not by coqc:
Definition f (x : t A) := match x with Top.c _ => 0 end. *)
(* assuming that this code is put in file.v, then
this third definition is accepted by coqc but not by coqtop (via ProofGeneral):
Definition f (x : t A) := match x with File.c _ => 0 end. *)
End S2.
Why the second definition is not accepted by coqc?
Is there a definition that can be accepted by both coqc and coqtop, while keeping c as a notation for (c A) in section S2?
Thanks for your help.
Frederic.
- [Coq-Club] definition accepted by coqc but not accepted by coqtop, Frederic Blanqui, 10/10/2012
- Re: [Coq-Club] definition accepted by coqc but not accepted by coqtop, Pierre Courtieu, 10/10/2012
- Re: [Coq-Club] definition accepted by coqc but not accepted by coqtop, Frederic Blanqui, 10/11/2012
- Re: [Coq-Club] definition accepted by coqc but not accepted by coqtop, AUGER Cédric, 10/11/2012
- Re: [Coq-Club] definition accepted by coqc but not accepted by coqtop, Pierre Courtieu, 10/11/2012
- Re: [Coq-Club] definition accepted by coqc but not accepted by coqtop, AUGER Cédric, 10/11/2012
- Re: [Coq-Club] definition accepted by coqc but not accepted by coqtop, Frederic Blanqui, 10/11/2012
- Re: [Coq-Club] definition accepted by coqc but not accepted by coqtop, Pierre Courtieu, 10/10/2012
Archive powered by MHonArc 2.6.18.