coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] import

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] import
Date: Tue, 22 Sep 2020 10:07:08 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f175.google.com
Ironport-phdr: 9a23:10xSZh/tYDBcWv9uRHKM819IXTAuvvDOBiVQ1KB21u0cTK2v8tzYMVDF4r011RmVBNqdsqkP0rCN++C4ACpcuMjH6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjTu8UMnIdvJKk9xgbXrnZGZu9awX9kKU+Jkxvz+8u9/YRv/zhMt/4k6sVNTbj0c6MkQLJCET8oKXo15MrltRnCSQuA+H4RWXgInxRLHgbI8gj0Uo/+vSXmuOV93jKaPdDtQrAvRTui9aZrRwT2hyoBKjU07XvYis10jKJcvRKhuxlyyJPabY2JKPZzeL7WcMgETmRdQMleSy1BApu9b4QRCeoBIf1YpJT5q1cXsBeyGRWgCObpxzRVhHH5wLc63vwuHgHI3gMuH9wAvnfJotvrKKgcXvu4zLXRzTjZc/9axSvx5YrOfxs8of+MR7Vwcc/JxEc1FgPKkE+QqZb7MDiIyOkNtHWb7/B8VeKulWEnthx6rz+3xsctlIbJnJgVxU7e+Splx4Y1OMe4SFJ6YdG6DZtdrC6aN45sTcMjR2Fkojo1yroDuZOieiUB1ZsoyQLFZfOdb4iI/gzsVPyXITpgmn9pZb2yihmv/EWhxeDxWNe53UpUoidZjtXBuG0B2h/c5MWESvVx40ev1SiP2g7T6uxJJUA5mLTFJ5I/3rM9ipweulnNEC/xnUX5lq6WdkM89+ip7eTneLTmqYWGO496kAHzNLkllM+nAekgLAQCQ2yW9f6/2bDj50H1XbRHg/wsnqXEsp3XJcIWrbOjDQBPyIYs8RO/Ai+m0NsGmXkHK0pIeBedgIjoP1HCOfH4DfOij1i1njdn2vLLM737DpXCKXjDl7jhfbJj5EJG1AUzytVf64pVCrEHPv3zRlf8uMLEAhI9KQC5wObqBM9g2o4fWG+DGLKVPaHSvFOQ4+IgOeiMZIsbuDbnLPgl4ubjjWc4mVADZ6mpx4UYZGqkEfRhPkWZe2bsgtYfHmcXpQc+Q+nqh0eDUT5XfXq9Q6U85jQjBIK8EYjDXpytgKCG3CqjApJWYXlGBkmQHnfsaoWLQOwBaDmSI89kijwLT6KtS44n1RG0tQ/10aBrLuTO+n5QiZW2/99sr8bXiBt6oTdzFoGW13yHZ2ByhGIBATEsivNRu0t4n2+C3LJijrRzEsFJ+/JET09uLZ/R1fZ3Tdv1Rxjdf9qUYFmjS9SiRzo2S4RikJc1f09hFoD63Vj41C2wDupQzuTTXcBmwufnx3H0Yv1F5TPezqB41gspR8JOMSutgastr1GOVb6MqF2QkuORTYpZ3CPJ8z3dn2+HvUUdUQopFKucAi1ZaUzRotD0oEjFSu32UOV1Ak560ceHb5ByRJjshFRCSu3kPY2HMW20kma0Qx2Pw+HVYQ==

You need to compile the first file with coqc and require it from the
other file. This should explain how to do it:

In short:
coqc Foo.v
will produce a Foo.vo file

and then you can use
Require Foo.
in the other file. The definitions of foo will be accessible via the
qualified names: e.g. "Foo.T" "Foo.f" etc.
You may consider doing
Require Import Foo.
if you want to use short names.

https://coq.inria.fr/distrib/current/refman/language/core/modules.html#
https://coq.inria.fr/tutorial/3-modules

Best,
Pierre Courtieu

Le mar. 22 sept. 2020 à 08:46, Patricia Peratto
<psperatto AT vera.com.uy> a écrit :
>
> I have defined some proofs in a file .v and I want to import
> it inside other file.
>
> How can I do this?
>
> Regards,
> Patricia

[Coq-Club] import, Patricia Peratto, 09/19/2020
- Re: [Coq-Club] import, Pierre Courtieu, 09/22/2020
  - Re: [Coq-Club] import, Théo Zimmermann, 09/22/2020
    - Re: [Coq-Club] import, Erik Martin-Dorel, 09/22/2020
- <Possible follow-up(s)>
- [Coq-Club] import, Patricia Peratto, 09/21/2020