下面的代码(当然不是完整的证明)尝试对依赖乘积进行模式匹配:
尝试执行时出现的错误如下:
Record fail : Set :=
mkFail {
i : nat ;
f : forall x, x < i -> nat
}.
Definition failomat : forall (m : nat) (f : forall x, x < m -> nat), nat.
Proof.
intros.
apply 0.
Qed.
Function fail_hard_omat fl : nat := failomat (i fl) (f fl).
Definition failhard fl : fail_hard_omat fl = 0.
refine ((fun fl =>
match fl with
| mkFail 0 _ => _
| mkFail (S n) _ => _
end) fl).
尝试执行时出现的错误如下:
Toplevel input, characters 0-125:
Error: Illegal application (Type Error):
The term "mkFail" of type
"forall i : nat, (forall x : nat, x < i -> nat) -> fail"
cannot be applied to the terms
"i" : "nat"
"f0" : "forall x : nat, x < i0 -> nat"
The 2nd term has type "forall x : nat, x < i0 -> nat"
which should be coercible to "forall x : nat, x < i -> nat".
看起来替换在某种情况下无法到达内部类型参数。