Module Qcert.Translation.Lang.DNNRCtotDNNRC

Require Import DNNRCSystem.
Require Import tDNNRCSystem.

Section DNNRCtotDNNRC.

  Section Top.
    Context {ftype: ForeignType.foreign_type}.
    Context {fr:foreign_runtime}.
    Context {bm:brand_model}.
    Context {ftyping: foreign_typing}.

    Definition dnnrc_to_dnnrc_typed_top (tdenv: tdbindings) (q:dnnrc) : option dnnrc_typed :=
      infer_dnnrc_base_type tdenv nil q.

  End Top.
  
End DNNRCtotDNNRC.