def CC.interp_var {s : Sig} (env : TypeEnv s) (x : Var Kind.var s) : ℕ

Interpret a variable in an environment to get its free variable index.

Equations

• CC.interp_var env (CC.Var.free n) = n
• CC.interp_var env (CC.Var.bound x_2) = env.lookup_var x_2

structure CC.Retype {s1 s2 : Sig} (env1 : TypeEnv s1) (σ : Subst s1 s2) (env2 : TypeEnv s2) : Prop

• var (x : BVar s1 Kind.var) : env1.lookup_var x = interp_var env2 (σ.var x)
• tvar (X : BVar s1 Kind.tvar) : env1.lookup_tvar X ≈ Ty.shape_val_denot env2 (σ.tvar X)
• cvar (C : BVar s1 Kind.cvar) : env1.lookup_cvar C = (σ.cvar C).subst (Subst.from_TypeEnv env2)

theorem CC.weaken_interp_var {s : Sig} {env : TypeEnv s} {n : ℕ} {x : Var Kind.var s} : interp_var env x = interp_var (env.extend_var n) (x.rename Rename.succ)

theorem CC.tweaken_interp_var {s : Sig} {env : TypeEnv s} {d : PreDenot} {x : Var Kind.var s} : interp_var env x = interp_var (env.extend_tvar d) (x.rename Rename.succ)

theorem CC.cweaken_interp_var {s : Sig} {env : TypeEnv s} {cs : CaptureSet ∅} {x : Var Kind.var s} : interp_var env x = interp_var (env.extend_cvar cs) (x.rename Rename.succ)

theorem CC.Retype.liftVar {a✝ : Sig} {env1 : TypeEnv a✝} {s2✝ : Sig} {σ : Subst a✝ s2✝} {env2 : TypeEnv s2✝} {x : ℕ} (ρ : Retype env1 σ env2) : Retype (env1.extend_var x) σ.lift (env2.extend_var x)

theorem CC.Retype.liftTVar {a✝ : Sig} {env1 : TypeEnv a✝} {s2✝ : Sig} {σ : Subst a✝ s2✝} {env2 : TypeEnv s2✝} {d : PreDenot} (ρ : Retype env1 σ env2) : Retype (env1.extend_tvar d) σ.lift (env2.extend_tvar d)

theorem CC.Retype.liftCVar {a✝ : Sig} {env1 : TypeEnv a✝} {s2✝ : Sig} {σ : Subst a✝ s2✝} {env2 : TypeEnv s2✝} {cs : CaptureSet ∅} (ρ : Retype env1 σ env2) : Retype (env1.extend_cvar cs) σ.lift (env2.extend_cvar cs)

@[irreducible]

def CC.retype_shape_val_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {σ : Subst s1 s2} {env2 : TypeEnv s2} (ρ : Retype env1 σ env2) (T : Ty TySort.shape s1) : Ty.shape_val_denot env1 T ≈ Ty.shape_val_denot env2 (T.subst σ)

Equations

• ⋯ = ⋯

def CC.retype_capturebound_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {σ : Subst s1 s2} {env2 : TypeEnv s2} (ρ : Retype env1 σ env2) (B : CaptureBound s1) : CaptureBound.denot env1 B = CaptureBound.denot env2 (B.subst σ)

Equations

• ⋯ = ⋯

def CC.retype_resolved_capture_set {s1 s2 : Sig} {env1 : TypeEnv s1} {σ : Subst s1 s2} {env2 : TypeEnv s2} (ρ : Retype env1 σ env2) (C : CaptureSet s1) : C.subst (Subst.from_TypeEnv env1) = (C.subst σ).subst (Subst.from_TypeEnv env2)

Equations

• ⋯ = ⋯

def CC.retype_captureset_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {σ : Subst s1 s2} {env2 : TypeEnv s2} (ρ : Retype env1 σ env2) (C : CaptureSet s1) : CaptureSet.denot env1 C = CaptureSet.denot env2 (C.subst σ)

Equations

• ⋯ = ⋯

@[irreducible]

def CC.retype_capt_val_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {σ : Subst s1 s2} {env2 : TypeEnv s2} (ρ : Retype env1 σ env2) (T : Ty TySort.capt s1) : Ty.capt_val_denot env1 T ≈ Ty.capt_val_denot env2 (T.subst σ)

Equations

• ⋯ = ⋯

@[irreducible]

def CC.retype_exi_val_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {σ : Subst s1 s2} {env2 : TypeEnv s2} (ρ : Retype env1 σ env2) (T : Ty TySort.exi s1) : Ty.exi_val_denot env1 T ≈ Ty.exi_val_denot env2 (T.subst σ)

Equations

• ⋯ = ⋯

def CC.retype_capt_exp_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {σ : Subst s1 s2} {env2 : TypeEnv s2} (ρ : Retype env1 σ env2) (T : Ty TySort.capt s1) : Ty.capt_exp_denot env1 T ≈ Ty.capt_exp_denot env2 (T.subst σ)

Equations

• ⋯ = ⋯

@[irreducible]

def CC.retype_exi_exp_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {σ : Subst s1 s2} {env2 : TypeEnv s2} (ρ : Retype env1 σ env2) (T : Ty TySort.exi s1) : Ty.exi_exp_denot env1 T ≈ Ty.exi_exp_denot env2 (T.subst σ)

Equations

• ⋯ = ⋯

def CC.Retype.open_arg {s : Sig} {env : TypeEnv s} {y : Var Kind.var s} : Retype (env.extend_var (interp_var env y)) (Subst.openVar y) env

Equations

• ⋯ = ⋯

theorem CC.open_arg_shape_val_denot {s : Sig} {env : TypeEnv s} {y : Var Kind.var s} {T : Ty TySort.shape (s,x)} : Ty.shape_val_denot (env.extend_var (interp_var env y)) T ≈ Ty.shape_val_denot env (T.subst (Subst.openVar y))

theorem CC.open_arg_capt_val_denot {s : Sig} {env : TypeEnv s} {y : Var Kind.var s} {T : Ty TySort.capt (s,x)} : Ty.capt_val_denot (env.extend_var (interp_var env y)) T ≈ Ty.capt_val_denot env (T.subst (Subst.openVar y))

theorem CC.open_arg_exi_val_denot {s : Sig} {env : TypeEnv s} {y : Var Kind.var s} {T : Ty TySort.exi (s,x)} : Ty.exi_val_denot (env.extend_var (interp_var env y)) T ≈ Ty.exi_val_denot env (T.subst (Subst.openVar y))

theorem CC.open_arg_exi_exp_denot {s : Sig} {env : TypeEnv s} {y : Var Kind.var s} {T : Ty TySort.exi (s,x)} : Ty.exi_exp_denot (env.extend_var (interp_var env y)) T ≈ Ty.exi_exp_denot env (T.subst (Subst.openVar y))

def CC.Retype.open_targ {s : Sig} {env : TypeEnv s} {S : Ty TySort.shape s} : Retype (env.extend_tvar (Ty.shape_val_denot env S)) (Subst.openTVar S) env

Equations

• ⋯ = ⋯

theorem CC.open_targ_shape_val_denot {s : Sig} {env : TypeEnv s} {S : Ty TySort.shape s} {T : Ty TySort.shape (s,X)} : Ty.shape_val_denot (env.extend_tvar (Ty.shape_val_denot env S)) T ≈ Ty.shape_val_denot env (T.subst (Subst.openTVar S))

theorem CC.open_targ_capt_val_denot {s : Sig} {env : TypeEnv s} {S : Ty TySort.shape s} {T : Ty TySort.capt (s,X)} : Ty.capt_val_denot (env.extend_tvar (Ty.shape_val_denot env S)) T ≈ Ty.capt_val_denot env (T.subst (Subst.openTVar S))

theorem CC.open_targ_exi_val_denot {s : Sig} {env : TypeEnv s} {S : Ty TySort.shape s} {T : Ty TySort.exi (s,X)} : Ty.exi_val_denot (env.extend_tvar (Ty.shape_val_denot env S)) T ≈ Ty.exi_val_denot env (T.subst (Subst.openTVar S))

theorem CC.open_targ_exi_exp_denot {s : Sig} {env : TypeEnv s} {S : Ty TySort.shape s} {T : Ty TySort.exi (s,X)} : Ty.exi_exp_denot (env.extend_tvar (Ty.shape_val_denot env S)) T ≈ Ty.exi_exp_denot env (T.subst (Subst.openTVar S))

def CC.Retype.open_carg {s : Sig} {env : TypeEnv s} {C : CaptureSet s} : Retype (env.extend_cvar (C.subst (Subst.from_TypeEnv env))) (Subst.openCVar C) env

Equations

• ⋯ = ⋯

theorem CC.open_carg_shape_val_denot {s : Sig} {env : TypeEnv s} {C : CaptureSet s} {T : Ty TySort.shape (s,C)} : Ty.shape_val_denot (env.extend_cvar (C.subst (Subst.from_TypeEnv env))) T ≈ Ty.shape_val_denot env (T.subst (Subst.openCVar C))

theorem CC.open_carg_exi_val_denot {s : Sig} {env : TypeEnv s} {C : CaptureSet s} {T : Ty TySort.exi (s,C)} : Ty.exi_val_denot (env.extend_cvar (C.subst (Subst.from_TypeEnv env))) T ≈ Ty.exi_val_denot env (T.subst (Subst.openCVar C))

theorem CC.open_carg_exi_exp_denot {s : Sig} {env : TypeEnv s} {C : CaptureSet s} {T : Ty TySort.exi (s,C)} : Ty.exi_exp_denot (env.extend_cvar (C.subst (Subst.from_TypeEnv env))) T ≈ Ty.exi_exp_denot env (T.subst (Subst.openCVar C))