Documentation Verification Report

Defs

📁 Source: Cslib/Languages/CombinatoryLogic/Defs.lean

Statistics

MetricCount
DefinitionsSKI, Red, applyList, size, «term_↠_», «term_⬝_», «term_⭢_», instDecidableEqSKI, decEq, instReprSKI, repr
11
TheoremsI, K, S, head, tail, ne, applyList_concat, mJoin_red_head, mJoin_red_tail, parallel_mRed, parallel_red
11
Total22

Cslib

Definitions

NameCategoryTheorems
SKI 📖CompData
81 mathmath: SKI.pred_def, SKI.sk_nequiv, SKI.ThAux_def, SKI.Polynomial.toSKI_correct, SKI.isZero_def, SKI.MRed.diamond, SKI.List.tail_def, SKI.List.prependZero_def, SKI.pair_def, SKI.List.cons_def, SKI.fixedPoint_correct, SKI.parallel_mRed, SKI.mRed_of_parallelReduction, SKI.natUnpairRight_def, SKI.Sab_irreducible, SKI.rec_zero, SKI.MRed.S, SKI.List.tailStep_def, SKI.C_head_mred, SKI.natUnpairLeft_def, SKI.predAux_def, SKI.unpaired_def, SKI.or_def, SKI.B_def, SKI.applyList_concat, SKI.confluent_redexFree, SKI.List.head_def, SKI.redexFree_iff_mred_eq, SKI.sqrt_def, SKI.cond_correct, SKI.and_def, SKI.rec_succ, SKI.snd_correct, SKI.redexFree_iff, SKI.le_def, SKI.R_def, SKI.parallelReduction_diamond, SKI.RedexFree.normal_red, SKI.church_red, SKI.Y_correct, SKI.rice', SKI.H_def, SKI.rec_def, SKI.mJoin_red_tail, SKI.fst_correct, SKI.unpaired_correct, SKI.Th_correct, SKI.MRed.head, SKI.rfindAboveAux_def, SKI.mJoin_red_equivalence, SKI.Ka_irreducible, SKI.MRed.tail, SKI.MRed.K, SKI.TF_nequiv, SKI.rfindAboveAux_base, SKI.join_parallelReduction_equivalence, SKI.natPair_def, SKI.MRed.I, SKI.mJoin_red_redexFree, SKI.List.nil_def, SKI.rotL_def, SKI.del_def, SKI.Sa_irreducible, SKI.mul_def, SKI.recAux_def, SKI.mJoin_red_head, SKI.List.headD_def, SKI.rfindAboveAux_step, SKI.C_def, SKI.rotR_def, SKI.churchK_injective, SKI.sqrtCond_def, SKI.add_def, SKI.parallel_red, SKI.Y_def, SKI.sub_def, SKI.Polynomial.elimVar_correct, SKI.redexFree_iff_evalStep, SKI.reflTransGen_parallelReduction_mRed, SKI.B_tail_mred, SKI.List.tailFold_correct
instDecidableEqSKI 📖CompOp
instReprSKI 📖CompOp

Cslib.SKI

Definitions

NameCategoryTheorems
Red 📖CompData
74 mathmath: pred_def, sk_nequiv, ThAux_def, Polynomial.toSKI_correct, isZero_def, MRed.diamond, List.tail_def, List.prependZero_def, pair_def, List.cons_def, fixedPoint_correct, parallel_mRed, mRed_of_parallelReduction, natUnpairRight_def, rec_zero, MRed.S, List.tailStep_def, C_head_mred, natUnpairLeft_def, predAux_def, unpaired_def, or_def, B_def, confluent_redexFree, List.head_def, redexFree_iff_mred_eq, sqrt_def, cond_correct, and_def, rec_succ, snd_correct, redexFree_iff, le_def, R_def, RedexFree.normal_red, church_red, Y_correct, rice', H_def, rec_def, mJoin_red_tail, fst_correct, unpaired_correct, Th_correct, MRed.head, rfindAboveAux_def, mJoin_red_equivalence, MRed.tail, MRed.K, TF_nequiv, rfindAboveAux_base, natPair_def, MRed.I, mJoin_red_redexFree, List.nil_def, rotL_def, del_def, mul_def, recAux_def, mJoin_red_head, List.headD_def, rfindAboveAux_step, C_def, rotR_def, sqrtCond_def, add_def, parallel_red, Y_def, sub_def, evalStep_right_correct, Polynomial.elimVar_correct, reflTransGen_parallelReduction_mRed, B_tail_mred, List.tailFold_correct
applyList 📖CompOp
2 mathmath: Polynomial.toSKI_correct, applyList_concat
size 📖CompOp
1 mathmath: churchK_size
«term_↠_» 📖CompOp
«term_⬝_» 📖CompOp
«term_⭢_» 📖CompOp

Theorems

NameKindAssumesProvesValidatesDepends On
applyList_concat 📖mathematicalapplyList
Cslib.SKI
app
mJoin_red_head 📖mathematicalRelation.MJoin
Cslib.SKI
Red
Relation.MJoin
Cslib.SKI
Red
app
MRed.head
mJoin_red_tail 📖mathematicalRelation.MJoin
Cslib.SKI
Red
Relation.MJoin
Cslib.SKI
Red
app
MRed.tail
parallel_mRed 📖mathematicalCslib.SKI
Red
Cslib.SKI
Red
app
MRed.head
MRed.tail
parallel_red 📖mathematicalRedCslib.SKI
Red
app

Cslib.SKI.MRed

Theorems

NameKindAssumesProvesValidatesDepends On
I 📖mathematicalCslib.SKI
Cslib.SKI.Red
Cslib.SKI.app
Cslib.SKI.I
K 📖mathematicalCslib.SKI
Cslib.SKI.Red
Cslib.SKI.app
Cslib.SKI.K
S 📖mathematicalCslib.SKI
Cslib.SKI.Red
Cslib.SKI.app
Cslib.SKI.S
head 📖mathematicalCslib.SKI
Cslib.SKI.Red
Cslib.SKI
Cslib.SKI.Red
Cslib.SKI.app
tail 📖mathematicalCslib.SKI
Cslib.SKI.Red
Cslib.SKI
Cslib.SKI.Red
Cslib.SKI.app

Cslib.SKI.Red

Theorems

NameKindAssumesProvesValidatesDepends On
ne 📖Cslib.SKI.Red

Cslib.instDecidableEqSKI

Definitions

NameCategoryTheorems
decEq 📖CompOp

Cslib.instReprSKI

Definitions

NameCategoryTheorems
repr 📖CompOp

---

← Back to Index