coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Making Modules work
- Date: Sun, 12 Apr 2020 19:24:48 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
- Ironport-phdr: 9a23:V4njERQ7r7HIFihGSLrlbPaL/dpsv+yvbD5Q0YIujvd0So/mwa67YhCN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnZBUin4YAFyP6H+HpPYp8WxzeG7vZPJMCtSgz/oSLx0LQ62qgCZnckfnZdlMq89ygrAszMccutQxHhoIle7lBP9oM67up9lpXcD88k9/tJNBP2pN58zSqZVWWx/bjIFofbzvByGdjOho3sRVmJPzEhNCgnBqhr/X9H4uW37sLglgXjIDYjNVbkxHA+aweJuQR7shj0AMmdgomrSi4p5h+RapkD4/kAt88vveIiQccFGUObFZ9pDHDhKW8cXXicHA4XuN4Y=
Hi;
I am really confused with Require, Export, Import, etc. I tried doing a Google search but I do not find any simple explanations.
What I want to do is to have two files Foo and Bar:
Definition magic : nat := 5.
End Foo.
Now, I want to be able to access magic inside Bar:
Module Bar.
Require Foo.
Import Foo.
Check Foo.magic.
Fail Check magic. (* How do I make this work? *)
End Bar.
Require Foo.
Import Foo.
Check Foo.magic.
Fail Check magic. (* How do I make this work? *)
End Bar.
What am I doing wrong?
- [Coq-Club] Making Modules work, Agnishom Chattopadhyay, 04/13/2020
- Re: [Coq-Club] Making Modules work, Tej Chajed, 04/13/2020
Archive powered by MHonArc 2.6.18.