我在 Coq 中定义了一个模块签名，它定义了几个符号。然而，当我尝试在签名之外使用这些符号时，Coq 失败了。下面给出了我的代码的简化版本。任何帮助将不胜感激。
Module Type Field_Axioms.
Delimit Scope Field_scope with F.
Open Scope Field_scope.
Parameter Element : Set.
Parameter addition : Element -> Element -> Element.
Infix " + " := addition : Field_scope. (* ASSIGNS THE "+" OPERATOR TO SCOPE. *)
End Field_Axioms
Module Type Ordered_Field_Axioms.
Declare Module Field : Field_Axioms.
Print Scope Field_scope. (* SHOWS THAT THE SCOPE IS EMPTY. *)
End Ordered_Field_Axioms.
最佳答案
您可以替换:
Declare Module Field : Field_Axioms.
与:
Declare Module Import Field : Field_Axioms.
关于coq - 如何使 Coq 中模块签名之外的注释可见？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/15720888/