Module Qcert.Translation.Lang.NRAtocNRAEnv

Require Import String.
Require Import List.
Require Import DataRuntime.
Require Import NRARuntime.
Require Import cNRAEnvRuntime.

Section NRAtocNRAEnv.
  Context {fr:foreign_runtime}.

  Section Top.
    Context (h:brand_relation_t).

    Definition nra_to_nraenv_core_top (q:nra) : nraenv_core :=
      nraenv_core_of_nra q.

    Theorem nra_to_nraenv_core_top_correct :
      forall q:nra, forall global_env:bindings,
          nra_eval_top h q global_env =
          nraenv_core_eval_top h (nra_to_nraenv_core_top q) global_env.
  End Top.
    
End NRAtocNRAEnv.