如何在Coq模塊簽名外顯示符號？

Question

我在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. 

Answer 1

您可以更換：

Declare Module Field : Field_Axioms. 

有：

Declare Module Import Field : Field_Axioms.