List

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

Statistics

Metric	Count
Definitions IsChurchList, IsChurchListPair, Cons, ConsPoly, Head, HeadD, HeadDPoly, Nil, NilPoly, PrependZero, PrependZeroPoly, SuccHead, Tail, TailPoly, TailStep, TailStepPoly, toChurch	17
Theorems fst, snd, cons_correct, cons_def, headD_correct, headD_def, head_correct, head_def, nil_correct, nil_def, prependZero_correct, prependZero_def, singleton_correct, succHead_correct, tailFold_correct, tailStep_correct, tailStep_def, tail_correct, tail_def, tail_init, toChurch_cons, toChurch_correct, toChurch_nil, isChurchListPair_trans, isChurchList_trans	25
Total	42

Cslib.SKI

Definitions

Name	Category	Theorems
IsChurchList 📖	MathDef	10 math math: IsChurchListPair.fst, isChurchList_trans, List.singleton_correct, List.succHead_correct, List.tail_correct, List.toChurch_correct, List.cons_correct, IsChurchListPair.snd, List.nil_correct, List.prependZero_correct
IsChurchListPair 📖	CompData	4 math math: isChurchListPair_trans, List.tailStep_correct, List.tail_init, List.tailFold_correct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isChurchListPair_trans 📖	mathematical	Cslib.SKI Red IsChurchListPair	IsChurchListPair	—	isChurchList_trans MRed.tail IsChurchListPair.fst IsChurchListPair.snd
isChurchList_trans 📖	mathematical	Cslib.SKI Red IsChurchList	IsChurchList	—	parallel_mRed MRed.head

Cslib.SKI.IsChurchListPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst 📖	mathematical	Cslib.SKI.IsChurchListPair	Cslib.SKI.IsChurchList Cslib.SKI.app Cslib.SKI.Fst	—	—
snd 📖	mathematical	Cslib.SKI.IsChurchListPair	Cslib.SKI.IsChurchList Cslib.SKI.app Cslib.SKI.Snd	—	—

Cslib.SKI.List

Definitions

Name	Category	Theorems
Cons 📖	CompOp	6 math math: prependZero_def, cons_def, singleton_correct, tailStep_def, toChurch_cons, cons_correct
ConsPoly 📖	CompOp	—
Head 📖	CompOp	2 math math: head_def, head_correct
HeadD 📖	CompOp	2 math math: headD_correct, headD_def
HeadDPoly 📖	CompOp	—
Nil 📖	CompOp	7 math math: tail_def, singleton_correct, toChurch_nil, nil_def, tail_init, nil_correct, tailFold_correct
NilPoly 📖	CompOp	—
PrependZero 📖	CompOp	2 math math: prependZero_def, prependZero_correct
PrependZeroPoly 📖	CompOp	—
SuccHead 📖	CompOp	1 math math: succHead_correct
Tail 📖	CompOp	2 math math: tail_def, tail_correct
TailPoly 📖	CompOp	—
TailStep 📖	CompOp	4 math math: tail_def, tailStep_def, tailStep_correct, tailFold_correct
TailStepPoly 📖	CompOp	—
toChurch 📖	CompOp	3 math math: toChurch_correct, toChurch_nil, toChurch_cons

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons_correct 📖	mathematical	Cslib.SKI.IsChurch Cslib.SKI.IsChurchList	Cslib.SKI.IsChurchList Cslib.SKI.app Cons	—	cons_def
cons_def 📖	mathematical	—	Cslib.SKI Cslib.SKI.Red Cslib.SKI.app Cons	—	Cslib.SKI.Polynomial.toSKI_correct
headD_correct 📖	mathematical	Cslib.SKI.IsChurch Cslib.SKI.IsChurchList	Cslib.SKI.IsChurch Cslib.SKI.app HeadD	—	Cslib.SKI.isChurch_trans headD_def Cslib.SKI.MRed.K
headD_def 📖	mathematical	—	Cslib.SKI Cslib.SKI.Red Cslib.SKI.app HeadD Cslib.SKI.K	—	Cslib.SKI.Polynomial.toSKI_correct
head_correct 📖	mathematical	Cslib.SKI.IsChurchList	Cslib.SKI.IsChurch Cslib.SKI.app Head	—	headD_correct Cslib.SKI.zero_correct
head_def 📖	mathematical	—	Cslib.SKI Cslib.SKI.Red Cslib.SKI.app Head Cslib.SKI.K Cslib.SKI.Zero	—	headD_def
nil_correct 📖	mathematical	—	Cslib.SKI.IsChurchList Nil	—	nil_def
nil_def 📖	mathematical	—	Cslib.SKI Cslib.SKI.Red Cslib.SKI.app Nil	—	Cslib.SKI.Polynomial.toSKI_correct
prependZero_correct 📖	mathematical	Cslib.SKI.IsChurchList	Cslib.SKI.IsChurchList Cslib.SKI.app PrependZero	—	Cslib.SKI.isChurchList_trans prependZero_def cons_correct Cslib.SKI.zero_correct
prependZero_def 📖	mathematical	—	Cslib.SKI Cslib.SKI.Red Cslib.SKI.app PrependZero Cons Cslib.SKI.Zero	—	Cslib.SKI.Polynomial.toSKI_correct
singleton_correct 📖	mathematical	Cslib.SKI.IsChurch	Cslib.SKI.IsChurchList Cslib.SKI.app Cons Nil	—	cons_correct nil_correct
succHead_correct 📖	mathematical	Cslib.SKI.IsChurchList	Cslib.SKI.IsChurchList Cslib.SKI.app SuccHead	—	head_correct Cslib.SKI.succ_correct Cslib.SKI.isChurchList_trans Cslib.SKI.B_tail_mred Cslib.SKI.B_def Cslib.SKI.C_def cons_correct nil_correct
tailFold_correct 📖	mathematical	Cslib.SKI.IsChurchList	Cslib.SKI Cslib.SKI.Red Cslib.SKI.app TailStep Cslib.SKI.MkPair Nil Cslib.SKI.IsChurchListPair	—	tail_init tailStep_correct Cslib.SKI.MRed.tail
tailStep_correct 📖	mathematical	Cslib.SKI.IsChurch Cslib.SKI.IsChurchListPair	Cslib.SKI.IsChurchListPair Cslib.SKI.app TailStep	—	Cslib.SKI.isChurchListPair_trans tailStep_def Cslib.SKI.isChurchList_trans Cslib.SKI.fst_correct Cslib.SKI.IsChurchListPair.snd Cslib.SKI.snd_correct cons_correct
tailStep_def 📖	mathematical	—	Cslib.SKI Cslib.SKI.Red Cslib.SKI.app TailStep Cslib.SKI.MkPair Cslib.SKI.Snd Cons	—	Cslib.SKI.Polynomial.toSKI_correct
tail_correct 📖	mathematical	Cslib.SKI.IsChurchList	Cslib.SKI.IsChurchList Cslib.SKI.app Tail	—	Cslib.SKI.isChurchList_trans tail_def tailFold_correct Cslib.SKI.MRed.tail Cslib.SKI.IsChurchListPair.fst
tail_def 📖	mathematical	—	Cslib.SKI Cslib.SKI.Red Cslib.SKI.app Tail Cslib.SKI.Fst TailStep Cslib.SKI.MkPair Nil	—	Cslib.SKI.Polynomial.toSKI_correct
tail_init 📖	mathematical	—	Cslib.SKI.IsChurchListPair Cslib.SKI.app Cslib.SKI.MkPair Nil	—	Cslib.SKI.isChurchList_trans Cslib.SKI.fst_correct nil_correct Cslib.SKI.snd_correct
toChurch_cons 📖	mathematical	—	toChurch Cslib.SKI.app Cons Cslib.SKI.toChurch	—	—
toChurch_correct 📖	mathematical	—	Cslib.SKI.IsChurchList toChurch	—	nil_correct cons_correct Cslib.SKI.toChurch_correct
toChurch_nil 📖	mathematical	—	toChurch Nil	—	—

---

← Back to Index