Section TCAMPTest.




  Program Definition EntityType : rtype
    := Rec Open [] _.

  Program Definition CustomerType : rtype
    := Rec Open [("age", Nat)
                 ; ("cid", Nat)
                 ; ("name", String)] _.

  Program Definition PurchaseType : rtype
    := Rec Open [("cid", Nat)
                 ; ("name", String)
                 ; ("pid", Nat)
                 ; ("quantity", Nat)] _.

  Definition CPTModelTypes :=
    [("Customer", CustomerType)
      ; ("Entity", EntityType)
      ; ("Purchase", PurchaseType)].

  Definition CPTContext
    := @mkBrand_context trivial_foreign_type CPRModel_relation CPTModelTypes (eq_refl _).

  Instance CPModel : brand_model
    := mkBrand_model CPRModel_relation CPTContext (eq_refl _) (eq_refl _).




  Lemma R1typed :
    rule_type (Brand (singleton "Entity")) (Coll String) R1.

End TCAMPTest.