coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: richard <richard.dapoigny AT univ-smb.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Problem with definitions scope in imported module
- Date: Sun, 22 Dec 2024 15:26:21 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=richard.dapoigny AT univ-smb.fr; spf=Pass smtp.mailfrom=richard.dapoigny AT univ-smb.fr; spf=None smtp.helo=postmaster AT smtpout02-ext4.partage.renater.fr
- Dkim-filter: OpenDKIM Filter v2.10.3 zmtaauth06.partage.renater.fr AE34E1000FB
- Ironport-sdr: 67682c9b_gFnwJOj7b9SfxSLukyJQ/akXZL1XyDU2zySQuE8al7Bv6RD McIBRnR/ivm7ZQnQAChmAmQYeDqgjR//ZXteWxA==
Thanks Mukesh for your prompt answer.
However, it does not work since in that case, variables in F3
become unknown.
Le 22/12/2024 à 14:03, mukesh tiwari a
écrit :
Hi Richard,
In F2.v you have a definition *Module
Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).*
and then the same in F3.v *Module
Mereology (M1 : UsualDecidableTypeFull) :=
DST_signature(M1).*. I suspect when you redefining Mereology
in F3 and subsequently importing F2.v, somehow it is causing
some confusion. Trying removing the definition *Module
Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).*
from F3.v and see if it works (I am not an expert in modules
so I cannot say for sure it is the case).
Best,
Mukesh
On Sun, 22 Dec 2024 at
12:15, richard <richard.dapoigny AT univ-smb.fr>
wrote:
Dear
coq members,I have the following problem with importing definitions with multiples
coq modules:
I have a file F1.v :
=====================================================================
Module DST_signature (M1 : UsualDecidableTypeFull).
Import M1.
...
End DST_signature.
=====================================================================
then a file F2.v (there is a file F1.vo) :
=====================================================================
Require Import F1.
Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).
(** Module Abstract *Structure **)
Module geometry_signature (M1 : UsualDecidableTypeFull).
Module basis_mereo := Mereology M1.
Import basis_mereo.
...
End geometry_signature.
=====================================================================
and finally a file F3.v (there is a file F2.vo and a file F1.vo) :
=====================================================================
Require Import F1.
Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).
(** Module Abstract *Structure **)
Module AbstractStructure (M1 : UsualDecidableTypeFull).
Module basis_inst := Mereology M1.
Import basis_inst.
...
End AbstractStructure.
Require Import F2.
Module Tarski_geom (M1 : UsualDecidableTypeFull).
Module basis_mereo := Mereology M1.
Import basis_mereo.
Module adt := AbstractStructure M1.
Import adt.
Module geom := geometry_signature M1.
Import geom.
...
Lemma test : forall A, η A balls -> η A (el Gspace). -> fail
...
End Tarski_geom.
=====================================================================
While there is no problem for all variables defined in F1 there seems to
be a problem with variables defined in F2 since the error is :
The term "Gspace" has type "basis_mereo.N" while it is expected to have
type "N". (Gspace is defined in F2)
If someone has an idea to solve the problem?
Thanks in advance,
Richard
- Re: [Coq-Club] Problem with definitions scope in imported module, richard, 12/22/2024
- Re: [Coq-Club] Problem with definitions scope in imported module, mukesh tiwari, 12/22/2024
- Re: [Coq-Club] Problem with definitions scope in imported module, richard, 12/22/2024
- Re: [Coq-Club] Problem with definitions scope in imported module, mukesh tiwari, 12/22/2024
- Re: [Coq-Club] Problem with definitions scope in imported module, Richard Dapoigny, 12/22/2024
- Re: [Coq-Club] Problem with definitions scope in imported module, Richard Dapoigny, 12/22/2024
- Re: [Coq-Club] Problem with definitions scope in imported module, mukesh tiwari, 12/22/2024
- Re: [Coq-Club] Problem with definitions scope in imported module, richard, 12/22/2024
- Re: [Coq-Club] Problem with definitions scope in imported module, mukesh tiwari, 12/22/2024
Archive powered by MHonArc 2.6.19+.