Context

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

Statistics

Metric	Count
Definitions Context, Context, Context, dom, instHasWellFormed, map_val, Context	7
Theorems haswellformed_def, map_val_keys, map_val_mem	3
Total	10

Cslib.CCS

Definitions

Name	Category	Theorems
Context 📖	CompData	—

Cslib.HasContext

Definitions

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

Cslib.LambdaCalculus.LocallyNameless

Definitions

Name	Category	Theorems
Context 📖	CompOp	4 math math: Context.haswellformed_def, Fsub.Env.Wf.map_subst, Fsub.Sub.map_subst, Fsub.Typing.subst_ty

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	6 math math: Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.map_subst_nmem, 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	—

---

← Back to Index