Как сделать нотации видимыми вне подписи модуля в Coq?

Я определил сигнатуру модуля в 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.

theorem-proving coq
person Larry Lee    schedule 30.03.2013    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете заменить:

Declare Module Field : Field_Axioms.

с:

Declare Module Import Field : Field_Axioms.
person Ptival    schedule 03.04.2013