“如果”不只是“匹配”的糖

Question

这两个定义之间有什么区别：

Definition f : forall x:bool, if x then bool else nat :=
  fun x => match x with
           | true => true
           | false => 42
           end.
(* ^ Accepted by Coq *)

Definition g : forall x:bool, if x then bool else nat :=
  fun x => if x then true else 42.
(* ^ REJECTED *)

以前，我以为这if实际上是糖，match但在依赖模式匹配方面似乎更具限制性，即使它也支持return语法。

这是故意的吗？如果是，规则是什么？

Answer 1

对我来说这看起来像是一个错误：如果你要求 Coq 打印f，它match会将if.

f = 
fun x : bool =>
if x as x0 return (if x0 then bool else nat) then true else 42
     : forall x : bool, if x then bool else nat

f is not universe polymorphic
Argument scope is [bool_scope]