Qcert.Basic.Typing.TBindings

Section TBindings.


  Context {ftype:foreign_type}.
  Context {m:brand_model}.

  Definition tbindings := list (string×rtype).

  Context {fdata:foreign_data}.
  Context {fdtyping:foreign_data_typing}.
  Definition bindings_type (b:list (string×data)) (t:tbindings)
    := Forall2 (fun xy1 xy2 ⇒
                      (fst xy1) = (fst xy2)
                  ∧ data_type (snd xy1) (snd xy2)) b t.

  Lemma bindings_type_has_type {env Γ} pf :
      bindings_type env Γ →
      data_type (drec env) (Rec Closed Γ pf).

  Lemma bindings_type_sort c τc :
    bindings_type c τc →
    bindings_type (rec_sort c) (rec_sort τc).

  Lemma bindings_type_Forall_normalized c τc :
    bindings_type c τc →
    Forall
      (fun d : string × data ⇒ data_normalized brand_relation_brands (snd d))
      c.

End TBindings.