Include M1
指在另一个模块(例如M)中包含M1的确切语义是什么?与在模块M内执行 Import M1
有何不同?更准确地说,以下命令的语义是什么:
Module Type M := M1 <+ M2 <+ M3.
Include M1
指在另一个模块(例如M)中包含M1的确切语义是什么?与在模块M内执行 Import M1
有何不同?更准确地说,以下命令的语义是什么:
Module Type M := M1 <+ M2 <+ M3.
总结俗语命令的语义:
Include M1
命令(可用于定义 模块 或 模块类型)要求 Coq 复制 M1
的所有字段。因此,它就像在环境模块(相应地,模块类型)中“复制并粘贴”M1
的内容。Import M1
命令(也可用于定义 模块 或 模块类型,但需要 M1
是一个 模块)允许使用其短标识符引用 M1
的字段(即,无需使用限定标识符 M1.field_name
)接下来,语法 Module Type M := M1 <+ M2 <+ M3
是以下方式的快捷方式:
Module Type M.
Include M1.
Include M2.
Include M3.
End M.
Import
的变体)。如果您在Include
和Import
之间犹豫不决,那么您应该首先尝试使用Import
,因为它会产生较轻的影响(它不会克隆指定模块的内容,而只是定义更短的名称)。Include
和Import
命令:(********************************************)
(* Example involving a parameterized module *)
(********************************************)
(* A signature *)
Module Type MT.
Parameter t : Type.
End MT.
(* A bigger signature *)
Module Type MT1.
Include MT.
Parameter u : t.
Parameter f : t -> t.
End MT1.
(* A parameterized module *)
Module F1 (M1 : MT1).
Import M1. (* => we can now write f rather than M1.f *)
Definition fu := f u.
End F1.
(* A module implementing MT1 *)
Module M1 <: MT1. (* => check the signature but don't make the module opaque *)
Definition t := nat.
Definition u := O.
Definition f := S.
End M1.
(* Instantiation *)
Module FM1 := F1 M1.
Compute FM1.fu.
我记得 Compute 是 Eval vm_compute in
的快捷方式
(********************************************)
(* Extra example: a parameterized signature *)
(* *)
(* It can be noted that this feature of Coq *)
(* module types has no equivalent in OCaml… *)
(********************************************)
Module Type MT2 (M : MT).
Parameter u : M.t.
Import M. (* => we can now write t rather than M.t *)
Parameter f : t -> t.
End MT2.
(* Another parameterized module *)
Module F2 (M : MT) (M2 : MT2 M).
Import M2.
Definition fu := f u.
End F2.
(* Modules implementing MT and MT2 *)
Module M <: MT.
Definition t := bool.
End M.
Module M2 <: MT2 M.
Definition u := false.
Definition f := negb.
End M2.
(* Instantiation *)
Module FM2 := F2 M M2.
Compute FM2.fu.