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.