coq - 强制成对

Question

为什么强制在对内不起作用？在我的项目中，我有从Footo的强制，如果我有一个但想要一个Bar，这很好用。但是如果我想要一对s，但有一对s，它就行不通了。FooBarBarFoo

Inductive Foo := foo.
Inductive Bar := fromFoo of Foo.

Coercion fromFoo : Foo >-> Bar.

(* This works *)
Definition bar : Bar := foo.
(* This fails *)
Fail Definition bars : (Bar * Bar) := (foo,foo).

为什么 Coq 不在这里插入强制转换？

标签： coq