Basic properties of the type system.
This module contains fundamental properties about:
- Context operations and lookups
- Subtyping and subsumption
- Typing judgments
theorem
CC.Ctx.lookup_tvar_det
{s : Sig}
{Γ : Ctx s}
{X : BVar s Kind.tvar}
{T1 T2 : Ty TySort.shape s}
:
Γ.LookupTVar X T1 → Γ.LookupTVar X T2 → T1 = T2
theorem
CC.Ctx.lookup_cvar_det
{s : Sig}
{Γ : Ctx s}
{c : BVar s Kind.cvar}
{cb1 cb2 : CaptureBound s}
:
Γ.LookupCVar c cb1 → Γ.LookupCVar c cb2 → cb1 = cb2
Renaming preserves closedness of capture sets.
If a renamed capture set is closed, the original is also closed.
Renaming preserves closedness of capture bounds.
If a renamed capture bound is closed, the original is also closed.
theorem
CC.HasType.use_set_is_closed
{a✝ : Sig}
{C : CaptureSet a✝}
{Γ : Ctx a✝}
{e : Exp a✝}
{T : Ty TySort.exi a✝}
(ht : C # Γ ⊢ e : T)
:
C.IsClosed
theorem
CC.HasType.exp_is_closed
{a✝ : Sig}
{C : CaptureSet a✝}
{Γ : Ctx a✝}
{e : Exp a✝}
{T : Ty TySort.exi a✝}
(ht : C # Γ ⊢ e : T)
:
e.IsClosed
theorem
CC.HasType.type_is_closed
{a✝ : Sig}
{C : CaptureSet a✝}
{Γ : Ctx a✝}
{e : Exp a✝}
{E : Ty TySort.exi a✝}
(ht : C # Γ ⊢ e : E)
:
E.IsClosed
theorem
CC.Ctx.lookup_var_exists
{s : Sig}
{Γ : Ctx s}
{x : BVar s Kind.var}
:
∃ (T : Ty TySort.capt s), Γ.LookupVar x T