Safety

📁 Source: Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean

Statistics

Metric	Count
Definitions PreservesTyping	1
Theorems preservation, progress, confluence_preservesTyping, redex_preservesTyping	4
Total	5

Cslib.LambdaCalculus.LocallyNameless.Stlc

Definitions

Name	Category	Theorems
PreservesTyping 📖	MathDef	1 math math: redex_preservesTyping

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
confluence_preservesTyping 📖	mathematical	Relation.Confluent Cslib.LambdaCalculus.LocallyNameless.Untyped.Term PreservesTyping Typing	Cslib.LambdaCalculus.LocallyNameless.Untyped.Term Typing	—	redex_preservesTyping
redex_preservesTyping 📖	mathematical	PreservesTyping	PreservesTyping Cslib.LambdaCalculus.LocallyNameless.Untyped.Term	—	—

Cslib.LambdaCalculus.LocallyNameless.Stlc.FullBeta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservation 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta	Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing	—	Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing.preservation_open
progress 📖	mathematical	Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing Cslib.LambdaCalculus.LocallyNameless.Stlc.Ty	Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Value Cslib.LambdaCalculus.LocallyNameless.Untyped.Term Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta	—	Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing.lc

---

← Back to Index