Documentation Verification Report

Typing

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

Statistics

Metric	Count
Definitions `Typing`, `Typing`	2
Theorems `abs_inv`, `canonical_form_abs`, `canonical_form_sum`, `canonical_form_tabs`, `inl_inv`, `inr_inv`, `narrow`, `subst_tm`, `subst_ty`, `tabs_inv`, `weaken`, `weaken_head`, `wf`	13
Total	15

Cslib.LambdaCalculus.LocallyNameless.Fsub

Definitions

Name	Category	Theorems
`Typing` 📖	CompData	—

Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_inv` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.abs` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.arrow`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.open_tm` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar`	—	—
`canonical_form_abs` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Value` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.arrow`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.abs`	—	—
`canonical_form_sum` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Value` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.sum`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.inl` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.inr`	—	—
`canonical_form_tabs` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Value` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.all`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.tabs`	—	—
`inl_inv` 📖	—	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.inl` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.sum`	—	—	—
`inr_inv` 📖	—	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.inr` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.sum`	—	—	—
`narrow` 📖	—	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub`	—	—	—
`subst_tm` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty`	`Cslib.HasSubstitution.subst` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.instHasSubstitution`	—	—
`subst_ty` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub`	`Cslib.LambdaCalculus.LocallyNameless.Context` `Cslib.LambdaCalculus.LocallyNameless.Context.map_val` `Cslib.HasSubstitution.subst` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.instHasSubstitutionTy` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.instHasSubstitutionTy` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.instHasSubstitution`	—	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.map_subst_nmem` `Cslib.LambdaCalculus.LocallyNameless.Context.map_val_mem`
`tabs_inv` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.tabs` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.all`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.open_ty` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.open'`	—	—
`weaken` 📖	—	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf`	—	—	—
`weaken_head` 📖	—	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	—	—	—
`wf` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.LC` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf`	—	`Cslib.HasFresh.fresh_exists`

Cslib.LambdaCalculus.LocallyNameless.Stlc

Definitions

Name	Category	Theorems
`Typing` 📖	CompData	—

---

← Back to Index