coq - "if"不仅仅是 "match"的糖

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]