Module Qcert.Data.DataSystem

Require Export DataRuntime.
Require Export DataTypes.

Class basic_model : Type
  := mk_basic_model {
         basic_model_runtime :> foreign_runtime
         ; basic_model_foreign_type :> foreign_type
         ; basic_model_brand_model :> brand_model
         ; basic_model_foreign_typing :> foreign_typing
       }.