Is there a way to use short names for theorems proved in a module ? I am thinking of theorems in
Require Import PeanoNat Fail Definition plop := mul_comm. Definition hop := Nat.mul_comm.
This doesn't work :
Require Import PeanoNat. Require Import Nat. Fail Definition plop := mul_comm.
You are confusing
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.
(And in case that was not clear,
Require Import X is just syntactic sugar for
Require X. Import X.)
Thank you ! Indeed, I had not understood this. This is clear now.
Last updated: Oct 04 2023 at 18:01 UTC