Stream: Coq users

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


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

Is there a way to use short names for theorems proved in a module ? I am thinking of theorems in Coq.Arith.PeanoNat.Nat.

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

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 file and then import the Nat module that is part of that 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: Jul 24 2024 at 11:01 UTC