Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Making Modules work

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Making Modules work


Chronological Thread 
  • 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:

Module Foo.

  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.

What am I doing wrong?



Archive powered by MHonArc 2.6.18.

Top of Page