在 Coq 中,
sig
被定义为:Inductive sig (A:Type) (P:A -> Prop) : Type :=
exist : forall x:A, P x -> sig P.
我的理解是:
"sig P" 是一种类型,其中 P 是一个函数,接收 A 类型的参数并返回 Prop 类型。该类型的定义使得如果 P x 成立,则类型为 A 的元素 x 属于 "sig P"。
proj1_sig
的定义为:
Definition proj1_sig (e:sig P) := match e with
| exist _ a b => a
end.
我不确定如何理解这个。是否可以有人提供更直观的理解?