coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Patricia Peratto" <psperatto AT adinet.com.uy>
- To: "coqclub" < coq-club AT inria.fr>
- Subject: [Coq-Club] module
- Date: Sun, 10 Jun 2012 15:03:46 -0300
|
Forgive me by the questions I make but I'm in
my
first Coq proof.
I have imported Coq.Structures.Equalities.
and
below it I import a Module with
Module Program1 (Import X:HasEq).
and Coq displays the message:
Error:X is not a module
but HasEq was defined in Equalities.
Regards
Patricia
|
- [Coq-Club] module, Patricia Peratto, 06/10/2012
- <Possible follow-up(s)>
- Fw: [Coq-Club] module, Patricia Peratto, 06/12/2012
- Re: Fw: [Coq-Club] module, Thomas Dinsdale-Young, 06/12/2012
Archive powered by MHonArc 2.6.18.