Reduction

📁 Source: Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean

Statistics

Metric	Count
Definitions Red, Value, body, «term_↠βᵛ_», «term_⭢βᵛ_»	5
Theorems lc, lc, body_case, body_let, open_tm_body	5
Total	10

Cslib.LambdaCalculus.LocallyNameless.Fsub.Term

Definitions

Name	Category	Theorems
Red 📖	CompData	1 math math: Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.progress
Value 📖	CompData	1 math math: Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.progress
body 📖	MathDef	2 math math: body_let, body_case
«term_↠βᵛ_» 📖	CompOp	—
«term_⭢βᵛ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
body_case 📖	mathematical	—	LC case body	—	—
body_let 📖	mathematical	—	LC let' body	—	—
open_tm_body 📖	mathematical	body LC	open_tm	—	—

Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Red

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lc 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Red	Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.LC	—	—

Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Value

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lc 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Value	Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.LC	—	—

---

← Back to Index