Module Qcert.Common.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_unary_op :> foreign_unary_op_typing
         ; foreign_typing_binary_op :> foreign_binary_op_typing
       }.