我读过一些教程if a then b else c代表match a with true => b | false => c end。然而，很奇怪的是，前者不检查类型a，而后者当然确保a是一个布尔值。例如，
Coq < Check if nil then 1 else 2.
if nil then 1 else 2
: nat
where
?A : [ |- Type]
Coq < Check match nil with true => 1 | false => 2 end.
Toplevel input, characters 33-38:
> Check match nil with true => 1 | false => 2 end.
> ^^^^^
Error: Found a constructor of inductive type bool while
a constructor of list is expected.
Why is if ... then ... else ...允许它的第一个参数是非布尔值以外的任何东西？是否存在超载情况？ (Locate "if".没有给出任何结果。）
让我引用一下Coq 参考手册 https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#if-then-else:
对于恰好具有两个构造函数的归纳类型以及不依赖于构造函数参数的模式匹配表达式，可以使用if ... then ... else ...符号。更一般地说，对于带有构造函数的归纳类型C1 and C2，我们有以下等价：
if term [dep_ret_type] then term1 else term2
相当于
match term [dep_ret_type] with
| C1 _ ... _ => term1 (* we cannot bind the arguments *)
| C2 _ ... _ => term2
end
如您所见，第一个构造函数被视为true价值。这是一个例子：
Definition is_empty {A : Type} (xs : list A) : bool :=
if xs then true else false.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
