2

いくつかの表記法を定義するモジュール シグネチャを 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.
4

1 に答える 1

2

次のものを置き換えることができます。

Declare Module Field : Field_Axioms.

と：

Declare Module Import Field : Field_Axioms.
于 2013-04-03T01:07:34.763 に答える