Module BasicSystem


Require Export BasicRuntime.
Require Export BasicTypes.

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
       }.