Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `Ty`, `«term_⊢_∶_»`, `«term_⤳_»`	3
Theorems `lc`, `perm`, `preservation_open`, `subst_aux`, `typing_subst_head`, `weaken`, `weaken_aux`	7
Total	10

Cslib.LambdaCalculus.LocallyNameless.Stlc

Definitions

Name	Category	Theorems
`Ty` 📖	CompData	—
`«term_⊢_∶_»` 📖	CompOp	—
`«term_⤳_»` 📖	CompOp	—

Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lc` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing`	`Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LC`	—	—
`perm` 📖	—	`Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing` `Cslib.LambdaCalculus.LocallyNameless.Stlc.Ty`	—	—	—
`preservation_open` 📖	—	`Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing` `Cslib.LambdaCalculus.LocallyNameless.Stlc.Ty` `Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open'` `Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.fvar`	—	—	`Cslib.HasFresh.fresh_exists`
`subst_aux` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing` `Cslib.LambdaCalculus.LocallyNameless.Context` `Cslib.LambdaCalculus.LocallyNameless.Stlc.Ty`	`Cslib.HasSubstitution.subst` `Cslib.LambdaCalculus.LocallyNameless.Untyped.Term` `Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.instHasSubstitutionTerm`	—	—
`typing_subst_head` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing` `Cslib.LambdaCalculus.LocallyNameless.Stlc.Ty`	`Cslib.HasSubstitution.subst` `Cslib.LambdaCalculus.LocallyNameless.Untyped.Term` `Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.instHasSubstitutionTerm`	—	—
`weaken` 📖	—	`Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing` `Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Context` `Cslib.LambdaCalculus.LocallyNameless.Stlc.Ty` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed`	—	—	—
`weaken_aux` 📖	—	`Cslib.LambdaCalculus.LocallyNameless.Stlc.Typing` `Cslib.LambdaCalculus.LocallyNameless.Context` `Cslib.LambdaCalculus.LocallyNameless.Stlc.Ty` `Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed`	—	—	—

---

← Back to Index