內部錯誤類型和外側部分

我有一個功能「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)

當我在S這個部分中有這個功能的時候沒問題。

但是我想在S部分的外面寫出函數incl_fl。以下是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」，但是我沒有成功。可否請你幫我寫下外號S之外的引理「incl_fl」？非常感謝你。

來源

2012-09-07 Quyen

我找到了答案。

Lemma incl_Fl : forall arity R R', Fl (HF (arity:=arity)) R [= R'.

來源

2012-09-07 04:39:38 Quyen

內部錯誤類型和外側部分

回答

相關問題