Context

📁 Source: Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean

Statistics

Metric	Count
Definitions Context, Context, Context, Context, Context, Context, dom, instHasWellFormed, map_val, Context, Context, Context	12
Theorems haswellformed_def, map_val_keys, map_val_mem	3
Total	15

Cslib.CCS

Definitions

Name	Category	Theorems
Context 📖	CompData	1 math math: Context.complete

Cslib.CLL.Proposition

Definitions

Name	Category	Theorems
Context 📖	CompData	—

Cslib.CLL.Sequent

Definitions

Name	Category	Theorems
Context 📖	CompOp	—

Cslib.HasContext

Definitions

Name	Category	Theorems
Context 📖	CompOp	1 math math: Cslib.Congruence.covariant

Cslib.HasHContext

Definitions

Name	Category	Theorems
Context 📖	CompOp	—

Cslib.LambdaCalculus.LocallyNameless

Definitions

Name	Category	Theorems
Context 📖	CompOp	8 math math: Context.haswellformed_def, Fsub.Ty.Wf.map_subst, Fsub.Env.Wf.map_subst, Fsub.Sub.map_subst, Stlc.Typing.weaken_aux, Fsub.Typing.subst_ty, Stlc.Typing.subst_aux, Stlc.Typing.weaken

Cslib.LambdaCalculus.LocallyNameless.Context

Definitions

Name	Category	Theorems
dom 📖	CompOp	—
instHasWellFormed 📖	CompOp	2 math math: Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.to_ok, haswellformed_def
map_val 📖	CompOp	7 math math: Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.map_subst_nmem, Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.map_subst, Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.map_subst, map_val_mem, Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.map_subst, map_val_keys, Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.subst_ty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
haswellformed_def 📖	mathematical	—	Cslib.HasWellFormed.wf Cslib.LambdaCalculus.LocallyNameless.Context instHasWellFormed	—	—
map_val_keys 📖	mathematical	—	map_val	—	—
map_val_mem 📖	mathematical	—	map_val	—	—

Cslib.LambdaCalculus.Named

Definitions

Name	Category	Theorems
Context 📖	CompData	1 math math: Context.complete

Cslib.Logic.HML.Proposition

Definitions

Name	Category	Theorems
Context 📖	CompData	—

Cslib.Logic.HML.Satisfies

Definitions

Name	Category	Theorems
Context 📖	CompData	—

---

← Back to Index