Qcert.Basic.TypeSystem.TBrandContext
Implicitly, everything derives from Any
Definition Any {ftype:foreign_type} {br:brand_relation} := Brand nil.
Section Brand_Context.
Context {ftype:foreign_type}.
Context {br:brand_relation}.
Section Brand_Context.
Context {ftype:foreign_type}.
Context {br:brand_relation}.
Represents a mapping from brands to types
Class brand_context :=
mkBrand_context {
brand_context_types : list (string×rtype);
brand_context_types_sorted : is_list_sorted ODT_lt_dec (domain brand_context_types) = true
}.
Lemma brand_context_nodup {m:brand_context} : NoDup (domain brand_context_types).
Lemma brand_context_ext m pf1 pf1':
mkBrand_context m pf1 = mkBrand_context m pf1'.
Lemma brand_context_fequal {m₁ m₂}:
@brand_context_types m₁ = @brand_context_types m₂ → m₁ = m₂.
Definition brand_context_Rec (m:brand_context) := Rec Open _ (brand_context_types_sorted).
Lemma brand_context_Rec_inj (m1 m2:brand_context) :
brand_context_Rec m1 = brand_context_Rec m2 → m1 = m2.
End Brand_Context.
End TBrandContext.
mkBrand_context {
brand_context_types : list (string×rtype);
brand_context_types_sorted : is_list_sorted ODT_lt_dec (domain brand_context_types) = true
}.
Lemma brand_context_nodup {m:brand_context} : NoDup (domain brand_context_types).
Lemma brand_context_ext m pf1 pf1':
mkBrand_context m pf1 = mkBrand_context m pf1'.
Lemma brand_context_fequal {m₁ m₂}:
@brand_context_types m₁ = @brand_context_types m₂ → m₁ = m₂.
Definition brand_context_Rec (m:brand_context) := Rec Open _ (brand_context_types_sorted).
Lemma brand_context_Rec_inj (m1 m2:brand_context) :
brand_context_Rec m1 = brand_context_Rec m2 → m1 = m2.
End Brand_Context.
End TBrandContext.