Basic

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

Statistics

Metric	Count
Definitions `And`, `AndPoly`, `B`, `BPoly`, `C`, `CPoly`, `CoeTermPolynomial`, `Cond`, `Del`, `DelPoly`, `FF`, `Fst`, `H`, `HPoly`, `IsBool`, `MkPair`, `Neg`, `Or`, `OrPoly`, `PairPoly`, `Polynomial`, `elimVar`, `eval`, `toSKI`, `varFreeToSKI`, `R`, `RPoly`, `RotL`, `RotLPoly`, `RotR`, `RotRPoly`, `Snd`, `TT`, `Th`, `ThAux`, `ThAuxPoly`, `Unpaired`, `UnpairedPoly`, `Y`, `YPoly`, `fixedPoint`, `«term&_»`, `«term_⬝'_»`	43
Theorems `B_def`, `B_tail_mred`, `C_def`, `C_head_mred`, `FF_correct`, `H_def`, `elimVar_correct`, `toSKI_correct`, `R_def`, `TT_correct`, `ThAux_def`, `Th_correct`, `Y_correct`, `Y_def`, `and_correct`, `and_def`, `cond_correct`, `del_def`, `fixedPoint_correct`, `fst_correct`, `isBool_trans`, `neg_correct`, `or_correct`, `or_def`, `pair_def`, `rotL_def`, `rotR_def`, `snd_correct`, `unpaired_correct`, `unpaired_def`	30
Total	73

Cslib.SKI

Definitions

Name	Category	Theorems
`And` 📖	CompOp	2 math math: `and_def`, `and_correct`
`AndPoly` 📖	CompOp	—
`B` 📖	CompOp	2 math math: `B_def`, `B_tail_mred`
`BPoly` 📖	CompOp	—
`C` 📖	CompOp	2 math math: `C_head_mred`, `C_def`
`CPoly` 📖	CompOp	—
`CoeTermPolynomial` 📖	CompOp	—
`Cond` 📖	CompOp	10 math math: `natUnpairRight_def`, `natUnpairLeft_def`, `or_def`, `cond_correct`, `and_def`, `rec_def`, `rfindAboveAux_def`, `natPair_def`, `recAux_def`, `sqrtCond_def`
`Del` 📖	CompOp	1 math math: `del_def`
`DelPoly` 📖	CompOp	—
`FF` 📖	CompOp	6 math math: `isZero_def`, `or_def`, `and_def`, `FF_correct`, `rice'`, `TF_nequiv`
`Fst` 📖	CompOp	5 math math: `pred_def`, `IsChurchListPair.fst`, `List.tail_def`, `unpaired_def`, `fst_correct`
`H` 📖	CompOp	2 math math: `H_def`, `Y_def`
`HPoly` 📖	CompOp	—
`IsBool` 📖	MathDef	8 math math: `neg_correct`, `isZero_correct`, `le_correct`, `or_correct`, `FF_correct`, `and_correct`, `TT_correct`, `isBool_trans`
`MkPair` 📖	CompOp	11 math math: `pred_def`, `List.tail_def`, `pair_def`, `List.tailStep_def`, `predAux_def`, `snd_correct`, `fst_correct`, `unpaired_correct`, `predAux_correct'`, `List.tail_init`, `List.tailFold_correct`
`Neg` 📖	CompOp	5 math math: `neg_correct`, `natUnpairRight_def`, `natUnpairLeft_def`, `natPair_def`, `sqrtCond_def`
`Or` 📖	CompOp	2 math math: `or_def`, `or_correct`
`OrPoly` 📖	CompOp	—
`PairPoly` 📖	CompOp	—
`Polynomial` 📖	CompData	—
`R` 📖	CompOp	1 math math: `R_def`
`RPoly` 📖	CompOp	—
`RotL` 📖	CompOp	1 math math: `rotL_def`
`RotLPoly` 📖	CompOp	—
`RotR` 📖	CompOp	1 math math: `rotR_def`
`RotRPoly` 📖	CompOp	—
`Snd` 📖	CompOp	5 math math: `List.tailStep_def`, `predAux_def`, `unpaired_def`, `snd_correct`, `IsChurchListPair.snd`
`TT` 📖	CompOp	6 math math: `isZero_def`, `or_def`, `and_def`, `rice'`, `TF_nequiv`, `TT_correct`
`Th` 📖	CompOp	1 math math: `Th_correct`
`ThAux` 📖	CompOp	1 math math: `ThAux_def`
`ThAuxPoly` 📖	CompOp	—
`Unpaired` 📖	CompOp	2 math math: `unpaired_def`, `unpaired_correct`
`UnpairedPoly` 📖	CompOp	—
`Y` 📖	CompOp	2 math math: `Y_correct`, `Y_def`
`YPoly` 📖	CompOp	—
`fixedPoint` 📖	CompOp	1 math math: `fixedPoint_correct`
`«term&_»` 📖	CompOp	—
`«term_⬝'_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`B_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `B`	—	`Polynomial.toSKI_correct`
`B_tail_mred` 📖	mathematical	`Cslib.SKI` `Red` `app`	`Cslib.SKI` `Red` `app` `B`	—	`B_def` `MRed.tail`
`C_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `C`	—	`Polynomial.toSKI_correct`
`C_head_mred` 📖	mathematical	`Cslib.SKI` `Red` `app`	`Cslib.SKI` `Red` `app` `C`	—	`C_def` `MRed.head`
`FF_correct` 📖	mathematical	—	`IsBool` `FF`	—	—
`H_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `H`	—	`Polynomial.toSKI_correct`
`R_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `R`	—	`Polynomial.toSKI_correct`
`TT_correct` 📖	mathematical	—	`IsBool` `TT`	—	`MRed.K`
`ThAux_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `ThAux`	—	`Polynomial.toSKI_correct`
`Th_correct` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Th`	—	`ThAux_def`
`Y_correct` 📖	mathematical	—	`Relation.MJoin` `Cslib.SKI` `Red` `app` `Y`	—	`Y_def` `H_def` `MRed.tail`
`Y_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Y` `H`	—	`Polynomial.toSKI_correct`
`and_correct` 📖	mathematical	`IsBool`	`IsBool` `app` `And`	—	`isBool_trans` `and_def` `cond_correct` `FF_correct`
`and_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `And` `Cond` `TT` `FF`	—	`Polynomial.toSKI_correct`
`cond_correct` 📖	mathematical	`IsBool`	`Cslib.SKI` `Red` `app` `Cond`	—	`rotR_def`
`del_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Del`	—	`Polynomial.toSKI_correct`
`fixedPoint_correct` 📖	mathematical	—	`Cslib.SKI` `Red` `fixedPoint` `app`	—	`H_def`
`fst_correct` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Fst` `MkPair`	—	`R_def` `cond_correct` `TT_correct`
`isBool_trans` 📖	mathematical	`Cslib.SKI` `Red` `IsBool`	`IsBool`	—	`MRed.head`
`neg_correct` 📖	mathematical	`IsBool`	`IsBool` `app` `Neg`	—	`isBool_trans` `cond_correct`
`or_correct` 📖	mathematical	`IsBool`	`IsBool` `app` `Or`	—	`isBool_trans` `or_def` `cond_correct`
`or_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Or` `Cond` `TT` `FF`	—	`Polynomial.toSKI_correct`
`pair_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Pair` `MkPair`	—	`Polynomial.toSKI_correct`
`rotL_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `RotL`	—	`Polynomial.toSKI_correct`
`rotR_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `RotR`	—	`Polynomial.toSKI_correct`
`snd_correct` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Snd` `MkPair`	—	`R_def` `cond_correct` `FF_correct`
`unpaired_correct` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Unpaired` `MkPair`	—	`unpaired_def` `parallel_mRed` `MRed.tail` `fst_correct` `snd_correct`
`unpaired_def` 📖	mathematical	—	`Cslib.SKI` `Red` `app` `Unpaired` `Fst` `Snd`	—	`Polynomial.toSKI_correct`

Cslib.SKI.Polynomial

Definitions

Name	Category	Theorems
`elimVar` 📖	CompOp	1 math math: `elimVar_correct`
`eval` 📖	CompOp	2 math math: `toSKI_correct`, `elimVar_correct`
`toSKI` 📖	CompOp	1 math math: `toSKI_correct`
`varFreeToSKI` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elimVar_correct` 📖	mathematical	`Cslib.SKI`	`Cslib.SKI` `Cslib.SKI.Red` `Cslib.SKI.app` `eval` `elimVar`	—	—
`toSKI_correct` 📖	mathematical	`Cslib.SKI`	`Cslib.SKI` `Cslib.SKI.Red` `Cslib.SKI.applyList` `toSKI` `eval`	—	`eval.congr_simp` `Cslib.SKI.applyList_concat` `Cslib.SKI.MRed.head` `elimVar_correct`

---

← Back to Index