Module tDNNRC

Section tDNNRC.

  Require Import BasicSystem.
  Require Import DNNRCSystem.
  
  Context {fruntime:foreign_runtime}.
  Context {ftype: ForeignType.foreign_type}.
  Context {br:brand_relation}.

  Record type_annotation {A:Set} : Set :=
    mkType_annotation {
        ta_base:A
        ; ta_inferred:drtype
        ; ta_required:drtype
                        
      }.

  Global Arguments type_annotation : clear implicits.
  Global Arguments mkType_annotation {A} ta_base ta_inferred ta_required.
  
  Definition dnnrc_dataframe_typed := @dnnrc _ (type_annotation unit) dataframe.

End tDNNRC.