Module Qcert.Translation.Lang.cNRAEnvtoNRAEnv
Require
Import
String
.
Require
Import
List
.
Require
Import
DataRuntime
.
Require
Import
cNRAEnvRuntime
.
Require
Import
NRAEnvRuntime
.
Section
cNRAEnvtoNRAEnv
.
Context
{
fr
:
foreign_runtime
}.
Section
Top
.
Context
(
h
:
brand_relation_t
).
Definition
nraenv_core_to_nraenv_top
(
q
:
nraenv_core
) :
nraenv
:=
nraenv_core_to_nraenv
q
.
Theorem
nraenv_core_to_nraenv_top_correct
:
forall
q
:
nraenv_core
,
forall
global_env
:
bindings
,
nraenv_core_eval_top
h
q
global_env
=
nraenv_eval_top
h
(
nraenv_core_to_nraenv_top
q
)
global_env
.
Proof.
intros
.
unfold
nraenv_core_eval_top
.
unfold
nraenv_eval_top
.
unfold
nraenv_core_to_nraenv_top
.
unfold
nraenv_eval
.
rewrite
nraenv_roundtrip
.
reflexivity
.
Qed.
End
Top
.
End
cNRAEnvtoNRAEnv
.