Documentation Verification Report

WellFormed

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

Statistics

Metric	Count
Definitions `Wf`, `Wf`	2
Theorems `map_subst`, `map_subst_nmem`, `narrow`, `strengthen`, `to_ok`, `lc`, `map_subst`, `narrow`, `narrow_cons`, `nmem_fv`, `of_bind_ty`, `of_env_sub`, `of_env_ty`, `open_lc`, `perm_env`, `strengthen`, `weaken`, `weaken_cons`, `weaken_head`	19
Total	21

Cslib.LambdaCalculus.LocallyNameless.Fsub.Env

Definitions

Name	Category	Theorems
`Wf` 📖	CompData	5 math math: `Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.wf`, `Wf.map_subst`, `Wf.strengthen`, `Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.wf`, `Wf.narrow`

Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_subst` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Context` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Context.map_val` `Cslib.HasSubstitution.subst` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.instHasSubstitutionTy`	—	—
`map_subst_nmem` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Context.dom` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	`Cslib.LambdaCalculus.LocallyNameless.Context.map_val` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.HasSubstitution.subst` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.instHasSubstitutionTy`	—	—
`narrow` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub`	—	—
`strengthen` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	—	—
`to_ok` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf`	`Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	—	—

Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty

Definitions

Name	Category	Theorems
`Wf` 📖	CompData	14 math math: `Wf.narrow`, `Wf.of_bind_ty`, `Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.wf`, `Wf.perm_env`, `Wf.of_env_sub`, `Wf.map_subst`, `Wf.strengthen`, `Wf.open_lc`, `Wf.weaken_cons`, `Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.wf`, `Wf.weaken_head`, `Wf.weaken`, `Wf.narrow_cons`, `Wf.of_env_ty`

Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lc` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.LC`	—	—
`map_subst` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub` `Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Context` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed` `Cslib.LambdaCalculus.LocallyNameless.Context.map_val` `Cslib.HasSubstitution.subst` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.instHasSubstitutionTy`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Context` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Context.map_val` `Cslib.HasSubstitution.subst` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.instHasSubstitutionTy` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.instHasSubstitution`	—	`Cslib.LambdaCalculus.LocallyNameless.Context.map_val_mem`
`narrow` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub` `Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub`	—	—
`narrow_cons` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub` `Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub`	—	—
`nmem_fv` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Context.dom` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fv`	—	—
`of_bind_ty` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf`	—	—
`of_env_sub` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf`	—	—
`of_env_ty` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf`	—	—
`open_lc` 📖	mathematical	`Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.all`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.open'`	—	`Cslib.HasFresh.fresh_exists`
`perm_env` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf`	—	—
`strengthen` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	—	—
`weaken` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	—	—
`weaken_cons` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	—	—
`weaken_head` 📖	mathematical	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.HasWellFormed.wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	`Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Env` `Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding`	—	—

---

← Back to Index