Qcert.Basic.Typing.TUtil
Section TUtil.
Context {fdata:foreign_data}.
Context {ftype:foreign_type}.
Context {m:brand_model}.
Definition tdot {A} (l:list (string × A)) (a:string) : option A := edot l a.
Definition tuneither (τ:rtype) : option (rtype × rtype).
Definition tuncoll (τ:rtype) : option rtype.
Lemma tuncoll_correct (τ τ':rtype) :
tuncoll τ = Some τ' →
τ = Coll τ'.
Definition tsingleton (τ:rtype) : option rtype.
Lemma tsingleton_correct (τ τ':rtype) :
tsingleton τ = Some (Option τ') →
τ = Coll τ'.
Definition tunrec (τ: rtype) : option (record_kind × (list (string × rtype))).
Lemma tunrec_correct k (τ:rtype) {l} :
tunrec τ = Some (k,l) →
{pf | τ = Rec k l pf}.
Definition trecConcat (τ₁ τ₂: rtype) : option rtype.
Definition tmergeConcat (τ₁ τ₂: rtype) : option rtype.
Definition tunrecdot (s:string) (τ:rtype) : option rtype.
Definition tunrecremove (s:string) (τ:rtype) : option rtype.
Definition tunrecproject (sl:list string) (τ:rtype) : option rtype.
Definition recConcat (τ₁ τ₂: rtype) : option rtype.
Definition mergeConcat (τ₁ τ₂: rtype) : option rtype.
Lemma RecMaybe_rec_concat_sort k l1 l2 :
RecMaybe k (rec_concat_sort l1 l2) = Some (Rec k (rec_concat_sort l1 l2) (drec_concat_sort_sorted l1 l2)).
Lemma Bottom_proj : Bottom₀ = ` Bottom.
Lemma Top_proj : Top₀ = ` Top.
Lemma Unit_proj : Unit₀ = ` Unit.
Lemma Nat_proj : Nat₀ = ` Nat.
Lemma Bool_proj : Bool₀ = ` Bool.
Lemma String_proj : String₀ = ` String.
Lemma Brand_canon {b} {τ₁:rtype} :` τ₁ = Brand₀ b → τ₁ = Brand b.
Lemma Bottom_canon {τ₁:rtype} :` τ₁ = Bottom₀ → τ₁ = Bottom.
Lemma Top_canon {τ₁:rtype} :` τ₁ = Top₀ → τ₁ = Top.
Lemma Unit_canon {τ₁:rtype} :` τ₁ = Unit₀ → τ₁ = Unit.
Lemma Nat_canon {τ₁:rtype} :` τ₁ = Nat₀ → τ₁ = Nat.
Lemma Bool_canon {τ₁:rtype} :` τ₁ = Bool₀ → τ₁ = Bool.
Lemma String_canon {τ₁:rtype} :` τ₁ = String₀ → τ₁ = String.
Lemma Coll_canon {τ₁ τ₀:rtype} :` τ₁ = Coll₀ (` τ₀) → τ₁ = Coll τ₀.
End TUtil.