inductive CC.Binding : Sig → Kind → Type

• var {s : Sig} : Ty TySort.capt s → Binding s Kind.var
• tvar {s : Sig} : Ty TySort.shape s → Binding s Kind.tvar
• cvar {s : Sig} : CaptureBound s → Binding s Kind.cvar

def CC.Binding.rename {s1 : Sig} {k : Kind} {s2 : Sig} : Binding s1 k → Rename s1 s2 → Binding s2 k

Equations

• (CC.Binding.var T).rename x✝ = CC.Binding.var (T.rename x✝)
• (CC.Binding.tvar T).rename x✝ = CC.Binding.tvar (T.rename x✝)
• (CC.Binding.cvar cb).rename x✝ = CC.Binding.cvar (cb.rename x✝)

inductive CC.Ctx : Sig → Type

• empty : Ctx ∅
• push {s : Sig} {k : Kind} : Ctx s → Binding s k → Ctx (s,,k)

def CC.Ctx.push_var {s : Sig} : Ctx s → Ty TySort.capt s → Ctx (s,x)

Equations

• x✝¹,x:x✝ = x✝¹.push (CC.Binding.var x✝)

def CC.Ctx.push_tvar {s : Sig} : Ctx s → Ty TySort.shape s → Ctx (s,X)

Equations

• x✝¹,X<:x✝ = x✝¹.push (CC.Binding.tvar x✝)

def CC.Ctx.push_cvar {s : Sig} : Ctx s → CaptureBound s → Ctx (s,C)

Equations

• x✝¹,C<:x✝ = x✝¹.push (CC.Binding.cvar x✝)

def CC.«term_,x:_» : Lean.TrailingParserDescr

Equations

• CC.«term_,x:_» = Lean.ParserDescr.trailingNode `CC.«term_,x:_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol ",x:") (Lean.ParserDescr.cat `term 66))

def CC.«term_,X<:_» : Lean.TrailingParserDescr

Equations

• CC.«term_,X<:_» = Lean.ParserDescr.trailingNode `CC.«term_,X<:_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol ",X<:") (Lean.ParserDescr.cat `term 66))

def CC.«term_,C<:_» : Lean.TrailingParserDescr

Equations

• CC.«term_,C<:_» = Lean.ParserDescr.trailingNode `CC.«term_,C<:_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol ",C<:") (Lean.ParserDescr.cat `term 66))

inductive CC.Binding.IsClosed {s : Sig} {k : Kind} : Binding s k → Prop

A binding is closed if the type it contains is closed.

• var {s : Sig} {T : Ty TySort.capt s} : T.IsClosed → (Binding.var T).IsClosed
• tvar {s : Sig} {T : Ty TySort.shape s} : T.IsClosed → (Binding.tvar T).IsClosed
• cvar {s : Sig} {cb : CaptureBound s} : cb.IsClosed → (Binding.cvar cb).IsClosed

inductive CC.Ctx.IsClosed {s : Sig} : Ctx s → Prop

A context is closed if all bindings in it are closed.

• empty : Ctx.empty.IsClosed
• push {x✝ : Sig} {Γ : Ctx x✝} {x✝¹ : Kind} {b : Binding x✝ x✝¹} : Γ.IsClosed → b.IsClosed → (Γ.push b).IsClosed

inductive CC.Ctx.LookupTVar {s : Sig} : Ctx s → BVar s Kind.tvar → Ty TySort.shape s → Prop

• here {x✝ : Sig} {Γ : Ctx x✝} {S : Ty TySort.shape x✝} : (Γ.push (Binding.tvar S)).LookupTVar BVar.here (S.rename Rename.succ)
• there {s : Sig} {k : Kind} {Γ : Ctx s} {X : BVar s Kind.tvar} {S : Ty TySort.shape s} {b : Binding s k} : Γ.LookupTVar X S → (Γ.push b).LookupTVar X.there (S.rename Rename.succ)

inductive CC.Ctx.LookupVar {s : Sig} : Ctx s → BVar s Kind.var → Ty TySort.capt s → Prop

• here {x✝ : Sig} {Γ : Ctx x✝} {T : Ty TySort.capt x✝} : (Γ.push (Binding.var T)).LookupVar BVar.here (T.rename Rename.succ)
• there {s : Sig} {k : Kind} {Γ : Ctx s} {x : BVar s Kind.var} {T : Ty TySort.capt s} {b : Binding s k} : Γ.LookupVar x T → (Γ.push b).LookupVar x.there (T.rename Rename.succ)

inductive CC.Ctx.LookupCVar {s : Sig} : Ctx s → BVar s Kind.cvar → CaptureBound s → Prop

• here {x✝ : Sig} {Γ : Ctx x✝} {cb : CaptureBound x✝} : (Γ.push (Binding.cvar cb)).LookupCVar BVar.here (cb.rename Rename.succ)
• there {s : Sig} {k : Kind} {x✝ : Sig} {Γ : Ctx x✝} {c : BVar x✝ Kind.cvar} {cb : CaptureBound x✝} {x✝¹ : Kind} {b0 : Binding x✝ x✝¹} {b : Binding s k} : Γ.LookupCVar c cb → (Γ.push b0).LookupCVar c.there (cb.rename Rename.succ)

inductive CC.Subcapt {s : Sig} : Ctx s → CaptureSet s → CaptureSet s → Prop

• sc_trans {s : Sig} {Γ : Ctx s} {C1 C2 C3 : CaptureSet s} : Subcapt Γ C1 C2 → Subcapt Γ C2 C3 → Subcapt Γ C1 C3
• sc_elem {s : Sig} {C1 C2 : CaptureSet s} {Γ : Ctx s} : C1.Subset C2 → Subcapt Γ C1 C2
• sc_union {s : Sig} {Γ : Ctx s} {C1 C3 C2 : CaptureSet s} : Subcapt Γ C1 C3 → Subcapt Γ C2 C3 → Subcapt Γ (C1.union C2) C3
• sc_var {s : Sig} {Γ : Ctx s} {x : BVar s Kind.var} {C : CaptureSet s} {S : Ty TySort.shape s} : Γ.LookupVar x (Ty.capt C S) → Subcapt Γ (CaptureSet.var (Var.bound x)) C
• sc_cvar {s : Sig} {Γ : Ctx s} {c : BVar s Kind.cvar} {C : CaptureSet s} : Γ.LookupCVar c (CaptureBound.bound C) → Subcapt Γ (CaptureSet.cvar c) C

inductive CC.Subbound {s : Sig} : Ctx s → CaptureBound s → CaptureBound s → Prop

• capset {s : Sig} {Γ : Ctx s} {C1 C2 : CaptureSet s} : Subcapt Γ C1 C2 → Subbound Γ (CaptureBound.bound C1) (CaptureBound.bound C2)
• top {s : Sig} {Γ : Ctx s} {B : CaptureBound s} : Subbound Γ B CaptureBound.unbound

inductive CC.Subtyp {s : Sig} {k : TySort} : Ctx s → Ty k s → Ty k s → Prop

• top {s : Sig} {Γ : Ctx s} {T : Ty TySort.shape s} : Subtyp Γ T Ty.top
• refl {s : Sig} {k : TySort} {Γ : Ctx s} {T : Ty k s} : Subtyp Γ T T
• trans {s : Sig} {k : TySort} {Γ : Ctx s} {T1 T2 T3 : Ty k s} (hT2 : T2.IsClosed) : Subtyp Γ T1 T2 → Subtyp Γ T2 T3 → Subtyp Γ T1 T3
• tvar {s : Sig} {Γ : Ctx s} {X : BVar s Kind.tvar} {S : Ty TySort.shape s} : Γ.LookupTVar X S → Subtyp Γ (Ty.tvar X) S
• arrow {s : Sig} {Γ : Ctx s} {T2 T1 : Ty TySort.capt s} {U1 U2 : Ty TySort.exi (s,x)} : Subtyp Γ T2 T1 → Subtyp (Γ,x:T2) U1 U2 → Subtyp Γ (T1.arrow U1) (T2.arrow U2)
• poly {s : Sig} {Γ : Ctx s} {S2 S1 : Ty TySort.shape s} {T1 T2 : Ty TySort.exi (s,X)} : Subtyp Γ S2 S1 → Subtyp (Γ,X<:S2) T1 T2 → Subtyp Γ (S1.poly T1) (S2.poly T2)
• cpoly {s : Sig} {Γ : Ctx s} {cb2 cb1 : CaptureBound s} {T1 T2 : Ty TySort.exi (s,C)} : Subbound Γ cb2 cb1 → Subtyp (Γ,C<:cb2) T1 T2 → Subtyp Γ (Ty.cpoly cb1 T1) (Ty.cpoly cb2 T2)
• capt {s : Sig} {Γ : Ctx s} {C1 C2 : CaptureSet s} {S1 S2 : Ty TySort.shape s} : Subcapt Γ C1 C2 → Subtyp Γ S1 S2 → Subtyp Γ (Ty.capt C1 S1) (Ty.capt C2 S2)
• exi {s : Sig} {Γ : Ctx s} {T1 T2 : Ty TySort.capt (s,C)} : Subtyp (Γ,C<:CaptureBound.unbound) T1 T2 → Subtyp Γ T1.exi T2.exi
• typ {s : Sig} {Γ : Ctx s} {T1 T2 : Ty TySort.capt s} : Subtyp Γ T1 T2 → Subtyp Γ T1.typ T2.typ

inductive CC.HasType {s : Sig} : CaptureSet s → Ctx s → Exp s → Ty TySort.exi s → Prop

• var {s : Sig} {x : BVar s Kind.var} {Γ : Ctx s} {S : Ty TySort.shape s} {C : CaptureSet s} : Γ.IsClosed → Γ.LookupVar x (Ty.capt C S) → CaptureSet.var (Var.bound x) # Γ ⊢ Exp.var (Var.bound x) : (Ty.capt (CaptureSet.var (Var.bound x)) S).typ
• abs {s : Sig} {Γ : Ctx s} {e : Exp (s,,Kind.var)} {T2 : Ty TySort.exi (s,,Kind.var)} {cs : CaptureSet s} {T1 : Ty TySort.capt s} : T1.IsClosed → (cs.rename Rename.succ ∪ CaptureSet.var (Var.bound BVar.here) # Γ,x:T1 ⊢ e : T2) → ∅ # Γ ⊢ Exp.abs cs T1 e : (Ty.capt cs (T1.arrow T2)).typ
• tabs {s : Sig} {Γ : Ctx s} {e : Exp (s,X)} {T : Ty TySort.exi (s,X)} {cs : CaptureSet s} {S : Ty TySort.shape s} : S.IsClosed → (cs.rename Rename.succ # Γ,X<:S ⊢ e : T) → ∅ # Γ ⊢ Exp.tabs cs S e : (Ty.capt cs (S.poly T)).typ
• cabs {s : Sig} {Γ : Ctx s} {e : Exp (s,C)} {T : Ty TySort.exi (s,C)} {cs : CaptureSet s} {cb : CaptureBound s} : cb.IsClosed → (cs.rename Rename.succ # Γ,C<:cb ⊢ e : T) → ∅ # Γ ⊢ Exp.cabs cs cb e : (Ty.capt cs (Ty.cpoly cb T)).typ
• pack {s : Sig} {x : Var Kind.var s} {Γ : Ctx s} {T : Ty TySort.capt (s,C)} {C : CaptureSet s} : C.IsClosed → (CaptureSet.var x # Γ ⊢ Exp.var x : (T.subst (Subst.openCVar C)).typ) → CaptureSet.var x # Γ ⊢ Exp.pack C x : T.exi
• app {s : Sig} {x : Var Kind.var s} {Γ : Ctx s} {T1 : Ty TySort.capt s} {T2 : Ty TySort.exi (s,x)} {y : Var Kind.var s} : (CaptureSet.var x # Γ ⊢ Exp.var x : (Ty.capt (CaptureSet.var x) (T1.arrow T2)).typ) → (CaptureSet.var y # Γ ⊢ Exp.var y : T1.typ) → CaptureSet.var x ∪ CaptureSet.var y # Γ ⊢ Exp.app x y : T2.subst (Subst.openVar y)
• tapp {s : Sig} {x : Var Kind.var s} {Γ : Ctx s} {T : Ty TySort.exi (s,X)} {S : Ty TySort.shape s} : S.IsClosed → (CaptureSet.var x # Γ ⊢ Exp.var x : (Ty.capt (CaptureSet.var x) (S.poly T)).typ) → CaptureSet.var x # Γ ⊢ Exp.tapp x S : T.subst (Subst.openTVar S)
• capp {s : Sig} {x : Var Kind.var s} {Γ : Ctx s} {T : Ty TySort.exi (s,C)} {D : CaptureSet s} : D.IsClosed → (CaptureSet.var x # Γ ⊢ Exp.var x : (Ty.capt (CaptureSet.var x) (Ty.cpoly (CaptureBound.bound D) T)).typ) → CaptureSet.var x # Γ ⊢ Exp.capp x D : T.subst (Subst.openCVar D)
• letin {s : Sig} {C : CaptureSet s} {Γ : Ctx s} {e1 : Exp s} {T : Ty TySort.capt s} {e2 : Exp (s,,Kind.var)} {U : Ty TySort.exi s} : (C # Γ ⊢ e1 : T.typ) → (C.rename Rename.succ # Γ,x:T ⊢ e2 : U.rename Rename.succ) → C # Γ ⊢ e1.letin e2 : U
• unpack {s : Sig} {C : CaptureSet s} {Γ : Ctx s} {t : Exp s} {T : Ty TySort.capt (s,C)} {u : Exp (s,,Kind.cvar,,Kind.var)} {U : Ty TySort.exi s} : (C # Γ ⊢ t : T.exi) → ((C.rename Rename.succ).rename Rename.succ # Γ,C<:CaptureBound.unbound,x:T ⊢ u : (U.rename Rename.succ).rename Rename.succ) → C # Γ ⊢ t.unpack u : U
• unit {s : Sig} {Γ : Ctx s} : ∅ # Γ ⊢ Exp.unit : (Ty.capt ∅ Ty.unit).typ
• btrue {s : Sig} {Γ : Ctx s} : ∅ # Γ ⊢ Exp.btrue : (Ty.capt ∅ Ty.bool).typ
• bfalse {s : Sig} {Γ : Ctx s} : ∅ # Γ ⊢ Exp.bfalse : (Ty.capt ∅ Ty.bool).typ
• read {s : Sig} {x : Var Kind.var s} {Γ : Ctx s} {C : CaptureSet s} : (CaptureSet.var x # Γ ⊢ Exp.var x : (Ty.capt C Ty.cell).typ) → CaptureSet.var x # Γ ⊢ Exp.read x : (Ty.capt ∅ Ty.bool).typ
• write {s : Sig} {x : Var Kind.var s} {Γ : Ctx s} {Cx : CaptureSet s} {y : Var Kind.var s} : (CaptureSet.var x # Γ ⊢ Exp.var x : (Ty.capt Cx Ty.cell).typ) → (CaptureSet.var y # Γ ⊢ Exp.var y : (Ty.capt ∅ Ty.bool).typ) → CaptureSet.var x ∪ CaptureSet.var y # Γ ⊢ Exp.write x y : (Ty.capt ∅ Ty.unit).typ
• cond {s : Sig} {C1 : CaptureSet s} {Γ : Ctx s} {x : Var Kind.var s} {Cb C2 : CaptureSet s} {e2 : Exp s} {T : Ty TySort.exi s} {C3 : CaptureSet s} {e3 : Exp s} : (C1 # Γ ⊢ Exp.var x : (Ty.capt Cb Ty.bool).typ) → (C2 # Γ ⊢ e2 : T) → (C3 # Γ ⊢ e3 : T) → C1 ∪ C2 ∪ C3 # Γ ⊢ Exp.cond x e2 e3 : T
• invoke {s : Sig} {x : Var Kind.var s} {Γ : Ctx s} {y : Var Kind.var s} : (CaptureSet.var x # Γ ⊢ Exp.var x : (Ty.capt (CaptureSet.var x) Ty.cap).typ) → (CaptureSet.var y # Γ ⊢ Exp.var y : (Ty.capt (CaptureSet.var y) Ty.unit).typ) → CaptureSet.var x ∪ CaptureSet.var y # Γ ⊢ Exp.app x y : (Ty.capt ∅ Ty.unit).typ
• subtyp {s : Sig} {C1 : CaptureSet s} {Γ : Ctx s} {e : Exp s} {E1 : Ty TySort.exi s} {C2 : CaptureSet s} {E2 : Ty TySort.exi s} : (C1 # Γ ⊢ e : E1) → Subcapt Γ C1 C2 → Subtyp Γ E1 E2 → C2.IsClosed → E2.IsClosed → C2 # Γ ⊢ e : E2

def CC.«term_#_⊢_:_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.