0

我很难弄清楚如何编写这段代码。

例如，我有一个签名，A一个函子作为参数，为了能够使用，我定义了一个模块实现签名Ca: ACBA

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 *)

并支持我有类型foo: string -> string list-> nat.

然后在End B.，我有一个错误Coq说：signature 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所以我的问题是我不知道在这种情况下如何提供论点。

在我的真实代码中，我使用Section并Record键入而不是Module.

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 成为公理......另一个解决方案是延迟提供 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 回答