Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `Binding`, `fv`, `Env`, `Term`, `fv_tm`, `fv_ty`, `Ty`, `fv`, `instInhabitedBinding`, `default`, `instInhabitedTy`, `default`	12
Theorems	0
Total	12

Cslib.LambdaCalculus.LocallyNameless.Fsub

Definitions

Name	Category	Theorems
`Binding` 📖	CompData	28 math math: `Sub.narrow`, `Typing.narrow`, `Ty.Wf.narrow`, `Sub.weaken_head`, `Sub.strengthen`, `Env.Wf.to_ok`, `Binding.subst_sub`, `Env.Wf.map_subst_nmem`, `Ty.Wf.map_subst`, `Sub.narrow_aux`, `Env.Wf.map_subst`, `Ty.Wf.strengthen`, `Typing.subst_tm`, `Typing.tabs_inv`, `Ty.Wf.weaken_cons`, `Typing.abs_inv`, `Sub.map_subst`, `Binding.subst_fresh`, `Sub.weaken`, `Env.Wf.strengthen`, `Ty.Wf.weaken_head`, `Ty.Wf.weaken`, `Typing.weaken`, `Ty.Wf.narrow_cons`, `Typing.subst_ty`, `Env.Wf.narrow`, `Binding.subst_ty`, `Typing.weaken_head`
`Env` 📖	CompOp	20 math math: `Sub.narrow`, `Typing.narrow`, `Ty.Wf.narrow`, `Sub.weaken_head`, `Sub.strengthen`, `Env.Wf.to_ok`, `Ty.Wf.map_subst`, `Sub.narrow_aux`, `Env.Wf.map_subst`, `Ty.Wf.strengthen`, `Typing.subst_tm`, `Sub.map_subst`, `Sub.weaken`, `Env.Wf.strengthen`, `Ty.Wf.weaken_head`, `Ty.Wf.weaken`, `Typing.weaken`, `Typing.subst_ty`, `Env.Wf.narrow`, `Typing.weaken_head`
`Term` 📖	CompData	28 math math: `Term.open_ty_subst_ty_intro`, `Term.open_tm_subst_ty`, `Term.openRec_tm_subst_tm`, `Term.open_ty_subst_tm`, `Typing.canonical_form_tabs`, `Typing.canonical_form_sum`, `Term.openRec_ty_subst_tm`, `Term.open_ty_subst_ty`, `Term.subst_tm_lc`, `Term.subst_ty_def`, `Term.subst_tm_fresh`, `Term.openRec_ty_subst_ty`, `Term.open_tm_subst_tm`, `Typing.progress`, `Typing.subst_tm`, `Term.subst_ty_lc`, `Term.openRec_ty_subst_ty_intro`, `Term.openRec_tm_subst_tm_intro`, `Term.open_tm_subst_tm_intro`, `Term.open_ty_subst_tm_var`, `Typing.canonical_form_abs`, `Term.open_ty_subst_ty_var`, `Term.subst_ty_fresh`, `Term.open_tm_subst_ty_var`, `Term.open_tm_subst_tm_var`, `Term.subst_tm_def`, `Typing.subst_ty`, `Term.openRec_tm_subst_ty`
`Ty` 📖	CompData	33 math math: `Ty.open_subst`, `Term.open_ty_subst_ty_intro`, `Term.open_tm_subst_ty`, `Ty.subst_def`, `Ty.open_subst_intro`, `Typing.canonical_form_tabs`, `Term.open_ty_subst_ty`, `Binding.subst_sub`, `Term.subst_ty_def`, `Ty.openRec_subst_intro`, `Env.Wf.map_subst_nmem`, `Ty.Wf.map_subst`, `Env.Wf.map_subst`, `Term.openRec_ty_subst_ty`, `Typing.inl_inv`, `Typing.tabs_inv`, `Typing.abs_inv`, `Term.subst_ty_lc`, `Term.openRec_ty_subst_ty_intro`, `Sub.map_subst`, `Binding.subst_fresh`, `Ty.subst_fresh`, `Ty.openRec_subst`, `Typing.canonical_form_abs`, `Typing.inr_inv`, `Ty.subst_lc`, `Term.open_ty_subst_ty_var`, `Term.subst_ty_fresh`, `Term.open_tm_subst_ty_var`, `Typing.subst_ty`, `Binding.subst_ty`, `Term.openRec_tm_subst_ty`, `Ty.open_subst_var`
`instInhabitedBinding` 📖	CompOp	—
`instInhabitedTy` 📖	CompOp	—

Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding

Definitions

Name	Category	Theorems
`fv` 📖	CompOp	—

Cslib.LambdaCalculus.LocallyNameless.Fsub.Term

Definitions

Name	Category	Theorems
`fv_tm` 📖	CompOp	—
`fv_ty` 📖	CompOp	—

Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty

Definitions

Name	Category	Theorems
`fv` 📖	CompOp	3 math math: `Wf.nmem_fv`, `nmem_fv_openRec`, `nmem_fv_open`

Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedBinding

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedTy

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index