У меня есть определение my_def1
:типы Кастинг в Coq
Require Import compcert.common.Memory.
Require Import compcert.common.Values.
Require Import compcert.lib.Integers.
Definition my_def1 (vl: list memval) : val :=
match proj_bytes vl with
| Some bl => Vint(Int.sign_ext 16 (Int.repr (decode_int bl)))
| None => Vundef
end.
Я хотел бы написать еще одно определение my_def2
похожее на my_def1
, как показано ниже, и добавить аксиому, что proj_bytes vl
всегда возвращают Some bl
, так:
Definition my_def2 (vl: list memval) : val :=
Vint(Int.sign_ext 16 (Int.repr (decode_int ((*?*)))))
end.
Мой вопрос, как я могу заполнить my_def2
и написать связанный axiom
о proj_bytes vl
?
Или вопрос в том, как я могу бросить от типа list memval
к list byte
[decode_int
принимает list byte
]?
А вот определение memval
:
Inductive memval : Type :=
Undef : memval
| Byte : byte -> memval
| Fragment : val -> quantity -> nat -> memval
Спасибо. Что касается аксиомы, я пытался написать ее как 'Axiom pb1: forall vl, proj_bytes vl = Some v.', который не распознал v. Не могли бы вы объяснить больше о его логике? –
Я имею в виду логику того, что вы написали. –
'{v | P} 'означает, что существует некоторое' v', такое, что 'P' выполняется. Вы также можете быть более тонкими, чтобы указать некоторую аксиому 'not_undefined vl', которая исключает нежелательные случаи, а затем переходите к анализу case. – ejgallego