0

たとえば、次のようなレコードタイプがあります。

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

の型を返すパターン マッチングがあります。たとえば、次のmatrixIntように呼び出しました(whereは の型を返します。pfunction_name pmatrixIntpconstargs

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

p2 つのフィールドを返すパターン マッチングを書くのを手伝ってくれませんconst; argsか? どうもありがとうございました！

4

2 に答える 2

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'.
于 2013-05-28T05:51:05.493 に答える