模式從一個記錄類型

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

謝謝你，我已經找到了答案：(const p)和(args p)

Answer 2

爲了記錄（雙關語意）：

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'.