Documentation Verification Report

Opening

πŸ“ Source: Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean

Statistics

MetricCount
DefinitionsinstHasSubstitutionTy, subst, LC, instHasSubstitution, instHasSubstitutionTy, openRec_tm, openRec_ty, open_tm, open_ty, subst_tm, subst_ty, Β«term_^α΅—α΅—_Β», Β«term_^α΅—α΅ž_Β», Β«term_⟦_↝_βŸ§α΅—α΅—Β», Β«term_⟦_↝_βŸ§α΅—α΅žΒ», LC, instHasSubstitution, open', openRec, subst, Β«term_^ᡞ_Β», Β«term_⟦_↝_⟧ᡞ»
22
Theoremssubst_fresh, subst_sub, subst_ty, openRec_tm_lc, openRec_tm_neq_eq, openRec_tm_subst_tm, openRec_tm_subst_tm_intro, openRec_tm_subst_ty, openRec_tm_ty_eq, openRec_ty_lc, openRec_ty_neq_eq, openRec_ty_subst_tm, openRec_ty_subst_ty, openRec_ty_subst_ty_intro, openRec_ty_tm_eq, open_tm_subst_tm, open_tm_subst_tm_intro, open_tm_subst_tm_var, open_tm_subst_ty, open_tm_subst_ty_var, open_ty_subst_tm, open_ty_subst_tm_var, open_ty_subst_ty, open_ty_subst_ty_intro, open_ty_subst_ty_var, subst_tm_def, subst_tm_fresh, subst_tm_lc, subst_ty_def, subst_ty_fresh, subst_ty_lc, nmem_fv_open, nmem_fv_openRec, openRec_lc, openRec_neq_eq, openRec_subst, openRec_subst_intro, open_subst, open_subst_intro, open_subst_var, subst_def, subst_fresh, subst_lc
43
Total65

Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding

Definitions

NameCategoryTheorems
instHasSubstitutionTy πŸ“–CompOp
7 mathmath: subst_sub, Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.map_subst_nmem, Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.map_subst, Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.map_subst, subst_fresh, Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.subst_ty, subst_ty
subst πŸ“–CompOpβ€”

Theorems

NameKindAssumesProvesValidatesDepends On
subst_fresh πŸ“–mathematicalfvCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy		β€”β€”
subst_sub πŸ“–mathematicalβ€”Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
sub
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.instHasSubstitution		β€”β€”
subst_ty πŸ“–mathematicalβ€”Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
ty
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.instHasSubstitution		β€”β€”

Cslib.LambdaCalculus.LocallyNameless.Fsub.Term

Definitions

NameCategoryTheorems
LC πŸ“–CompData
5 mathmath: body_let, Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.wf, Red.lc, body_case, Value.lc
instHasSubstitution πŸ“–CompOp
12 mathmath: openRec_tm_subst_tm, open_ty_subst_tm, openRec_ty_subst_tm, subst_tm_lc, subst_tm_fresh, open_tm_subst_tm, Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.subst_tm, openRec_tm_subst_tm_intro, open_tm_subst_tm_intro, open_ty_subst_tm_var, open_tm_subst_tm_var, subst_tm_def
instHasSubstitutionTy πŸ“–CompOp
12 mathmath: open_ty_subst_ty_intro, open_tm_subst_ty, open_ty_subst_ty, subst_ty_def, openRec_ty_subst_ty, subst_ty_lc, openRec_ty_subst_ty_intro, open_ty_subst_ty_var, subst_ty_fresh, open_tm_subst_ty_var, Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.subst_ty, openRec_tm_subst_ty
openRec_tm πŸ“–CompOp
4 mathmath: openRec_tm_subst_tm, openRec_tm_subst_tm_intro, openRec_tm_lc, openRec_tm_subst_ty
openRec_ty πŸ“–CompOp
4 mathmath: openRec_ty_subst_tm, openRec_ty_subst_ty, openRec_ty_lc, openRec_ty_subst_ty_intro
open_tm πŸ“–CompOp
7 mathmath: open_tm_subst_ty, open_tm_body, open_tm_subst_tm, Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.abs_inv, open_tm_subst_tm_intro, open_tm_subst_ty_var, open_tm_subst_tm_var
open_ty πŸ“–CompOp
6 mathmath: open_ty_subst_ty_intro, open_ty_subst_tm, open_ty_subst_ty, Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.tabs_inv, open_ty_subst_tm_var, open_ty_subst_ty_var
subst_tm πŸ“–CompOp
1 mathmath: subst_tm_def
subst_ty πŸ“–CompOp
1 mathmath: subst_ty_def
Β«term_^α΅—α΅—_Β» πŸ“–CompOpβ€”
Β«term_^α΅—α΅ž_Β» πŸ“–CompOpβ€”
Β«term_⟦_↝_βŸ§α΅—α΅—Β» πŸ“–CompOpβ€”
Β«term_⟦_↝_βŸ§α΅—α΅žΒ» πŸ“–CompOpβ€”

Theorems

NameKindAssumesProvesValidatesDepends On
openRec_tm_lc πŸ“–mathematicalLCopenRec_tmβ€”β€”
openRec_tm_neq_eq πŸ“–β€”openRec_tmβ€”β€”β€”
openRec_tm_subst_tm πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution
openRec_tm		β€”β€”
openRec_tm_subst_tm_intro πŸ“–mathematicalfv_tmopenRec_tm
Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution
fvar		β€”β€”
openRec_tm_subst_ty πŸ“–mathematicalβ€”Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
openRec_tm		β€”β€”
openRec_tm_ty_eq πŸ“–β€”openRec_tm
openRec_ty		β€”β€”β€”
openRec_ty_lc πŸ“–mathematicalLCopenRec_tyβ€”β€”
openRec_ty_neq_eq πŸ“–β€”openRec_tyβ€”β€”β€”
openRec_ty_subst_tm πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution
openRec_ty		β€”β€”
openRec_ty_subst_ty πŸ“–mathematicalCslib.LambdaCalculus.LocallyNameless.Fsub.Ty.LCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
openRec_ty
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.instHasSubstitution		β€”β€”
openRec_ty_subst_ty_intro πŸ“–mathematicalfv_tyopenRec_ty
Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar		β€”β€”
openRec_ty_tm_eq πŸ“–β€”openRec_ty
openRec_tm		β€”β€”β€”
open_tm_subst_tm πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution
open_tm		β€”openRec_tm_subst_tm
open_tm_subst_tm_intro πŸ“–mathematicalfv_tmopen_tm
Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution
fvar		β€”openRec_tm_subst_tm_intro
open_tm_subst_tm_var πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution
open_tm
fvar		β€”β€”
open_tm_subst_ty πŸ“–mathematicalβ€”Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
open_tm		β€”openRec_tm_subst_ty
open_tm_subst_ty_var πŸ“–mathematicalβ€”Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
open_tm
fvar		β€”β€”
open_ty_subst_tm πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution
open_ty		β€”openRec_ty_subst_tm
open_ty_subst_tm_var πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution
open_ty
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar		β€”open_ty_subst_tm
open_ty_subst_ty πŸ“–mathematicalCslib.LambdaCalculus.LocallyNameless.Fsub.Ty.LCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
open_ty
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.instHasSubstitution		β€”openRec_ty_subst_ty
open_ty_subst_ty_intro πŸ“–mathematicalfv_tyopen_ty
Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar		β€”openRec_ty_subst_ty_intro
open_ty_subst_ty_var πŸ“–mathematicalCslib.LambdaCalculus.LocallyNameless.Fsub.Ty.LCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy
open_ty
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar		β€”β€”
subst_tm_def πŸ“–mathematicalβ€”subst_tm
Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution		β€”β€”
subst_tm_fresh πŸ“–mathematicalfv_tmCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution		β€”β€”
subst_tm_lc πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
instHasSubstitution		β€”β€”
subst_ty_def πŸ“–mathematicalβ€”subst_ty
Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy		β€”β€”
subst_ty_fresh πŸ“–mathematicalfv_tyCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy		β€”β€”
subst_ty_lc πŸ“–mathematicalLC
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.LC		Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Term
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitutionTy		β€”β€”

Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty

Definitions

NameCategoryTheorems
LC πŸ“–CompData
1 mathmath: Wf.lc
instHasSubstitution πŸ“–CompOp
15 mathmath: open_subst, subst_def, open_subst_intro, Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.open_ty_subst_ty, Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.subst_sub, openRec_subst_intro, Wf.map_subst, Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_ty_subst_ty, Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.map_subst, subst_fresh, openRec_subst, subst_lc, Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.subst_ty, Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.subst_ty, open_subst_var
open' πŸ“–CompOp
5 mathmath: open_subst, open_subst_intro, Wf.open_lc, Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.tabs_inv, open_subst_var
openRec πŸ“–CompOp
3 mathmath: openRec_subst_intro, openRec_lc, openRec_subst
subst πŸ“–CompOp
1 mathmath: subst_def
Β«term_^ᡞ_Β» πŸ“–CompOpβ€”
Β«term_⟦_↝_⟧ᡞ» πŸ“–CompOpβ€”

Theorems

NameKindAssumesProvesValidatesDepends On
nmem_fv_open πŸ“–β€”fv
open'		β€”β€”nmem_fv_openRec
nmem_fv_openRec πŸ“–β€”fv
openRec		β€”β€”β€”
openRec_lc πŸ“–mathematicalLCopenRecβ€”β€”
openRec_neq_eq πŸ“–β€”openRecβ€”β€”β€”
openRec_subst πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitution
openRec		β€”β€”
openRec_subst_intro πŸ“–mathematicalfvopenRec
Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitution
fvar		β€”β€”
open_subst πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitution
open'		β€”openRec_subst
open_subst_intro πŸ“–mathematicalfvopen'
Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitution
fvar		β€”openRec_subst_intro
open_subst_var πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitution
open'
fvar		β€”β€”
subst_def πŸ“–mathematicalβ€”subst
Cslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitution		β€”β€”
subst_fresh πŸ“–mathematicalfvCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitution		β€”β€”
subst_lc πŸ“–mathematicalLCCslib.HasSubstitution.subst
Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty
instHasSubstitution		β€”β€”

---

← Back to Index