0

私は関数" HF"を持っていますセクション内にタイプがありますS

Open S.
HF: forall f : dup_sig Sig, dup_ar f = ASignature.arity (F f)
End S.

Signature: Type
Sig: Signature    
dp_Sig : Signature
dup_sig : Signature -> Signature
F : dup_sig Sig -> Sig
dup_symb : Signature -> Type
dup_ar : forall Sig : Signature, dup_symb Sig -> nat
ASignature.arity : forall s : Signature, s -> nat

補題を書きたい：

Lemma incl_fl : forall R R, Fl HF R [= R'.

どこ

Fl: forall (S1 S2 : Signature) (F : S1 -> S2),
       (forall f : S1, ASignature.arity f = ASignature.arity (F f)) ->
       list (ATrs.rule S1) -> list (ATrs.rule S2)

セクション内にこの関数があればOKSです。

incl_flしかし、セクションの外に関数を書きたいと思いSます。HFこれが外側のセクションのタイプですS。

HF: forall (arity : symbol -> nat) (f : dup_sig (Sig arity)),
    dup_ar f = ASignature.arity (F f)

Lemma incl_fl : forall arity R R', Fl HF R [= R'.

""でエラーが発生しましたHF：

The term "HF" has type
 "forall (arity : symbol -> nat) (f : dup_sig (Sig arity)),
  dup_ar f = ASignature.arity (F f)" while it is expected to have type
 "forall f : ?35524, ASignature.arity f = ASignature.arity (?35526 f)".

arityこの関数" "にを追加する場所を見つけようとしましたが、HF成功しません。incl_flセクションの外に見出語""を書くのを手伝ってくれませんSか。どうもありがとうございます。

4

1 に答える 1

1

私は答えを見つけました。

Lemma incl_Fl : forall arity R R', Fl (HF (arity:=arity)) R [= R'.
于 2012-09-07T04:39:38.417 に答える