0

このコードの書き方を理解するのに苦労しています。

たとえば、署名Aがあり、ファンクターがパラメーターとしてC取りa: A、使用できるように、署名を実装Cするモジュールを定義しますBA

Require Import String.
Module Type A.
  Parameter toto : string -> nat. 
End A.

Module C (Import a : A).
 ...
End C.

Module B <: A.
      Definition toto (s: string) := foo s.
End B. (* COQ error *)

とサポート I have typefoo: string -> string list-> nat.

次に、次のように言うとEnd B.エラーが発生します。Coqsignature components for label toto do not match: types differ.

または別の方法:

Module B.
 Definition too (s : string) := foo s.
End B.

Module Export D := C B.

で同じエラーが発生しますD

string listの定義で引数を指定しなかったため、問題は理解できましたtoto。

string listしたがって、私の問題は、この場合にどのように引数を提供できるかわからないことです。

私の実際のコードでは、の代わりにSectionandを使用していました。RecordModule

Record A : Type := mkA { too : string -> nat}.

それから私はSection

Section B.
 Variable l: string list.
 Definition too (s: string) := foo s l.
 Definition A := mkA too.
End B.

Bモジュールでファンクターを正しく書く方法を書いたり、理解したりするのを手伝ってくれませんか? string listモジュールで変数を定義/宣言できる方法はありますか? また、 で定義した後、Coqに抽出しOCamlます。

4

1 に答える 1

1

いつでもこれを行うことができます：

Require Import String.

Parameter foo: string -> list string -> nat.

Module Type A.

  Parameter toto : string -> nat. 

End A.

Module B <: A.

  Variable (* or Parameter, or Axiom *) ls : list string.

  Definition toto (s: string) := foo s ls.

End B.

しかし、ls を公理にしているという私の理解では、もう 1 つの解決策は、ls の提供を遅らせることです。

ModuleType HasListString.

  Parameter ls : list string.

End HasListString.

Module B(LS: HasListString) : A.

  Definition toto (s: string) := foo s LS.ls.

End B.

ただし、これは必要なものではないかもしれません。コンテキストがなければ、より適切なアドバイスを提供することは困難です。

于 2013-03-27T14:37:29.417 に答える