coq - 来自 Record 类型的模式匹配

Question

我有一个记录类型，例如：

 Record matrixInt : Type := mkMatrixInt {
    const : vector nat dim;
    args : vector (matrix dim dim) argCnt
  }.

我有一个模式匹配，它返回的类型matrixInt，我称之为p例如：（其中function_name p将返回一个类型matrixInt。我想p分成 2 个字段：const和args，例如我想要的草稿代码：

Definition my_function cons arg p :=
match function_name p with 
 | const => const + cons
 | args => args + arg
end.

您能否帮我编写p返回 2 个字段的模式匹配const; args？非常感谢！

Answer 1

为了记录（双关语）：

Record test :=
{ T : Type
; t : T
}.

(* The fields names are indeed accessor functions *)
Definition foo (x : test) : T x := t x.

(* you can destruct a record by matching against its data constructor *)
Definition bar (x : test) : T x :=
  match x as _x return T _x with
  | Build_test T' t' => t'
  end.

(* You can even destruct a record with a let *)
Definition baz (x : test) : T x :=
  let (T', t') as _x return T _x := x in t'.

Answer 2

谢谢我找到了答案：(const p)和(args p)