Qcert.CAMP.Typing.TCAMPSugar

Section TCAMPSugar.





  Context {m:basic_model}.

  Lemma PTCast τc Γ br bs :
    [τc&Γ] |= pcast br ; (Brand bs) ~> (Brand br).

  Lemma PTSingleton τc Γ τ :
    [τc&Γ] |= psingleton ; (Coll τ) ~> τ.

  Lemma PTmapall τc {Γ : tbindings} {τ₁ τ₂ : rtype} {p : pat} :
    NoDup (domain Γ) →
    ([τc&Γ] |= p; τ₁ ~> τ₂) → [τc&Γ] |= mapall p; Coll τ₁ ~> Coll τ₂.


  Lemma PTmapall_inv τc {Γ : tbindings} {τ₁ τ₂ : rtype} {p : pat} :
    RSort.is_list_sorted ODT_lt_dec (domain Γ) = true →
    [τc&Γ] |= mapall p; τ₁ ~> τ₂ →
                       ∃ τ₁' τ₂',
                         τ₁ = Coll τ₁' ∧
                         τ₂ = Coll τ₂' ∧
                         ([τc&Γ] |= p; τ₁' ~> τ₂').

End TCAMPSugar.