コック：強制の定義でエラーが発生しました

Question

は、あなたがエラーを修正することができます：

​​

私は

Coercion f (u:Arg) (x y z: Arg -> Prop) (t:x u /\ y u /\ z u): x u. tauto. Defined. Print f. 

Answer 1

部分的な答えから用語を取るとき、私は同じエラーを取得しています：あなたのfun t => @proj1 (x u) (y u /\ z u) t用語はですタイプx u /\ y u /\ z u -> x /\ uと入力します。あなたは強制的に型式がx uになるようにしたいので、関数x u /\ y u /\ z uをx uにするために関数に与える必要があります。

fun t => proj1 tのため混乱していると思います。混乱を避けるために、この変数の名前をfun foobar => proj1 foobarのような新しい名前に変更すると、実際にはt引数を使用することはありません。

したがって、全体の用語は(fun t => @proj1 (x u) (y u /\ z u) t) tであり、Definitionで動作します。しかし、Coercionの場合、次のメッセージが表示されます。

c is defined 
Warning: c does not respect the uniform inheritance condition 

Error: Cannot find the target class.