шаблон согласования с типом записи

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