Module Qcert.Data.ForeignTyping

Require Export Types.
Require Export ForeignRuntime.
Require Export ForeignDataTyping.
Require Export ForeignOperatorsTyping.

Class foreign_typing
      {fruntime:foreign_runtime}
      {ftype:foreign_type}
      {model:brand_model}
  : Type
  := mk_foreign_typing {
          foreign_typing_data :> foreign_data_typing
         ; foreign_typing_operators :> foreign_operators_typing
       }.