Stream: Coq users

Topic: ✔ Using short names of theorems in a Module (eg PeanoNat....


view this post on Zulip Guillaume Melquiond (Oct 04 2022 at 05:04):

Just Import Nat.

view this post on Zulip Pierre Rousselin (Oct 04 2022 at 05:31):

This doesn't work :

Require Import PeanoNat.
Require Import Nat.
Fail Definition plop := mul_comm.

view this post on Zulip Guillaume Melquiond (Oct 04 2022 at 05:37):

You are confusing Require and Import. Require loads a file, while Import puts the content of a module into scope. So, when you write Require Import Nat, you are telling Coq to load a file named Nat.vo and then to put its content into scope. What I was telling you was to do Require Import PeanoNat. Import Nat., that is, load the PeanoNat.vo and then import the Nat module that is in its file.

view this post on Zulip Guillaume Melquiond (Oct 04 2022 at 05:38):

(And in case that was not clear, Require Import X is just syntactic sugar for Require X. Import X.)

view this post on Zulip Pierre Rousselin (Oct 04 2022 at 05:50):

Thank you ! Indeed, I had not understood this. This is clear now.


Last updated: Jan 27 2023 at 00:03 UTC