Trust

Axioms come from the Lean kernel (Lean (version 4.34.0-rc1, x86_64-w64-windows-gnu, commit 3447a668783dbce1a8fdb97101dd067687b2b418, Release)): the constants each declaration depends on, as Lean's collectAxioms reports them. Standard axioms are propext, Classical.choice and Quot.sound.

Lake environment and dependency-pin digest: 6a543372efa49e0d.

Verification scope: all declaration-bearing files; 19 of 19 eligible files selected, 815 declarations requested.

Rendering mode: clean content-bound cache results only; 1 selected files had no reusable result and remain UNKNOWN. No Lean process was started for those misses during this static-site build.

Per-file probe bounds: 1800 seconds. A resource stop is UNKNOWN, never a failed proof.

no axioms: 26
standard axioms: 59
sorry: 0
extra axioms: 0
unknown: 730

What the badges mean

no axioms: Lean's kernel checked the proof, and it rests on nothing but Lean's rules.
standard axioms: Checked by the kernel, using only propext, Classical.choice or Quot.sound: the three axioms nearly all of mathematics in Lean uses.
extra axioms: Checked by the kernel, but it assumes something the project declared with `axiom`. It is only as true as those assumptions.
depends on sorry: Not proved: somewhere in it, or in something it uses, a proof was left out (`sorry`).
trust unknown: Lean did not check it: Lean was not run, the file did not elaborate, or Lean has no constant by that name.

Files outside this Lean pass (1)

book/TPiL/TypeClasses.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering

Trust UNKNOWN declarations (651)

types, book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.propext book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
thm₁ book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
thm₂ book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.mem book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.setext book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.mem book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.setext book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.empty book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.inter book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.inter_self book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.inter_empty book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.empty_inter book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Set.inter.comm book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
f book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
g book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
f_eq_g book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
val book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
tteq book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
val book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Quot book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Quot.mk book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Quot.ind book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Quot.lift book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
mod7Rel book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
f book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
f_respects book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Quot.sound book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.Setoid book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.Setoid.refl book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.Setoid.symm book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.Setoid.trans book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.of book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.Quotient book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.refl book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.symm book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.trans book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.is_equivalence book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.refl book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.symm book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.trans book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.is_equivalence book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.uprodSetoid book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mk book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.refl book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.symm book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.trans book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.is_equivalence book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.uprodSetoid book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mk book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.refl book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.symm book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.trans book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.is_equivalence book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.uprodSetoid book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mk book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mk_eq_mk book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.refl book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.symm book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.eqv.trans book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.is_equivalence book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.uprodSetoid book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mk book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mk_eq_mk book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mem_fn book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mem_swap book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mem_respects book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mem book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mem_mk_left book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mem_mk_right book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.UProd.mem_or_mem_of_mem_mk book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.extfun book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.extfun_app book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.extfun book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.extfun_app book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.Nonempty book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.choice book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.is book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.choice book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.indefiniteDescription book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.choose book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.choose_spec book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.inhabited_of_nonempty book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.em book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.em book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.propComplete book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.Hidden.Decidable book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.linv book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
Hidden.linv_comp_self book/TPiL/AxiomsComputation.lean trust unknown: Lean has no constant by this name
m book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
n book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
b1 book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
b2 book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
α book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
β book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
F book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
G book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
α book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
β book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
α book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
F book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
F book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
f book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
g book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
whatever book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
b book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
f book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
g book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
to book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
double book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
double book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
double book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
double book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
pi book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
add book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
double book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
add book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
greater book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
double book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
doTwice book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
compose book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
compose book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
double book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
square book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Natural book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Natural book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
five book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
twice_double book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
twice_double book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
t book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
foo book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
compose book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
doTwice book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
doThrice book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
compose book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
doTwice book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
doThrice book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
compose book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
doTwice book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
doThrice book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
cons book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
cons book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
f book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
g book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
h1 book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
h2 book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.cons book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.nil book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.append book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.cons book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.nil book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.append book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
as book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
bs book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.cons book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.nil book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.append book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
as book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
bs book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.cons book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.nil book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
Lst.append book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
as book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
bs book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
ident book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
ident book/TPiL/DependentTypeTheory.lean trust unknown: Lean has no constant by this name
TPiL.projectDir book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.hasAtLeastM book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.hasAtLeast book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.LineType book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.lineType book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.oneCodeStr book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.codeStrs book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.commentContents book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.showGoals book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.strOrName book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.keywords book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.tactics book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.leanLits book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
TPiL.suggest book/TPiL/Examples.lean trust unknown: Lean has no constant by this name
sub1 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
isZero book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
sub1 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
isZero book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
sub1 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
isZero book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
swap book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
bar book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Hidden.not book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Hidden.not_not book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
sub2 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
sub2 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
sub2 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
sub2 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
bar book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Hidden.and book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Hidden.or book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Hidden.cond book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
tail book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
data book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
tail1 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
tail2 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
f1 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
f2 book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
bar book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
add_zero book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
add_succ book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
zero_add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
mul book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
zero_add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
fib book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
fibFast book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
fibFast book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
fib book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
append book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
listAdd book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
replicate book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
replicate book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
length_replicate book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
replicate book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
length_replicate book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
r' book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
f book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div_lemma book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div.F book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div_lemma book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div.F book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div_lemma book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div.F book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
natToBin book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
ack book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
ack book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
takeWhile book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
takeWhile book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div_lemma book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
div book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
ack book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
natToBin book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
unsound book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
ack book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
ack_gt_zero book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
ack book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
ack_gt_zero book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
f book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
f book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
f_or book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
f book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
f_or book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
even_eq_not_odd book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Even book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Odd book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
not_odd_zero book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
even_of_odd_succ book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
odd_of_even_succ book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Term book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Term book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
sample book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Term book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Term.numConsts book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
map book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
zip book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
unzip book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
tail book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
families book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.tailAux book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.tail book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.head book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.tail book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.eta book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.map book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.zip book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.zipWith book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
ImageOf book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
inverse book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
inverse' book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.add book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.head book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.tail book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.eta book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.map book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Vect.zip book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
isNotZero book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
isNotZero book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
filter book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
bar₁ book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
bar₂ book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
bar₃ book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
bar₄ book/TPiL/InductionAndRecursion.lean trust unknown: Lean has no constant by this name
Foo book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Foo book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
numberOfDay book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
numberOfDay book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
in book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.next book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.previous book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.next book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.previous book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.next_previous book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.next book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.previous book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.next_previous book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Bool book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.and book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Prod book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Sum book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Prod book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.fst book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.snd book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.prod_example book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.sum_example book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Prod book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Sum book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Prod book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Color book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.yellow book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Semigroup book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Sigma book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Option book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Inhabited book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.False book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.True book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.And book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Or book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Exists book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Subtype book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Subtype book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat.add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat.add_zero book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat.add_succ book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.zero_add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.zero_add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.add_assoc book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.add_assoc book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.add_comm book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.succ_add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat.add_zero book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat.add_succ book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat.zero_add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.succ_add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.add_comm book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List.append book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List.nil_append book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List.cons_append book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List.append book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List.nil_append book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List.cons_append book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List.append_nil book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.List.append_assoc book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.length book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.append book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.BinaryTree book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.CBTree book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.CBTree.succ book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.CBTree.toCBTree book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.CBTree.omega book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.f book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Tuple book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.f book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.myTuple book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Foo book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.silly book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Foo book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.silly book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Foo book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.silly book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Foo book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.silly book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.zero_add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.zero_add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat.toNat book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Nat.ofNat book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.zero_zero book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.add_zero book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.add_succ book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.zero_add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.succ_add book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.add_comm book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.add_assoc book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.foo book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Vect book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.Eq book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.subst book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.subst book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.subst book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.symm book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.trans book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.Hidden.congr book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.definitions, book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.type book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.types book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Weekday.definitions book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Tree book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.length book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.reverse book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
Weekday.Term book/TPiL/InductiveTypes.lean trust unknown: Lean has no constant by this name
x book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
double book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
t2 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
Foo.bar book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
Foo.bar book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
Foo.bar book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
String.add book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
Bool.add book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
add book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
Foo.bar book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
isPrefix book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
List.isPrefix_self book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
isPrefix book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
List.isPrefix_self book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
isPrefix book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
List.isPrefix_self book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
isPrefix book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
List.isPrefix_self book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
isPrefix book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
instLe book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
f book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
f book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
f' book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
reflexive book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
symmetric book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
transitive book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
Euclidean book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
th1 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
th2 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
th3 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
reflexive book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
symmetric book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
transitive book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
Euclidean book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
th1 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
th2 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
th3 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
wobble book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
wobble book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
foo book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.compose book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.compose book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.compose book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.compose book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.Ex2.id1 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.Ex2.listId book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.Ex2.id2 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.Ex2.id3 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.Ex2.id4 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.Ex2.id5 book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.Ex3.f book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.sum book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.f book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.g book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.Term book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.getBinderName book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
{lit}`Nat`.getBinderType book/TPiL/InteractingWithLean.lean trust unknown: Lean has no constant by this name
Implies book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Proof book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Implies book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Implies book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Proof book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
and_commut book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Implies book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Proof book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
modus_ponens book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Implies book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Proof book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
implies_intro book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
is book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
hp book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t2 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
unsound book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
ex book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t1 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
t2 book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
type book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Foo book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Bar book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
Foo.bar book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
and_swap book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
and_swap book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
long book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
dne book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
dne book/TPiL/PropositionsAndProofs.lean trust unknown: Lean has no constant by this name
T book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
T book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
T book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
T book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
T book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
divides book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
divides_trans book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
divides_mul book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
gex1 book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
gex2 book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
gex3 book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
gex4 book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
of book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
IsEven book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
IsEven book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
even_plus_even book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
IsEven book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
even_plus_even book/TPiL/QuantifiersEquality.lean trust unknown: Lean has no constant by this name
of book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
data book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.p book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point.add book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.p book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.q book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point.smul book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.p book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.xs book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.f book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.MyStruct book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.object book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.p book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point3 book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.q book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.r book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Color book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.ColorPoint book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.Point book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.RGBValue book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.RedGreenPoint book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.p book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
with.rgp book/TPiL/StructuresAndRecords.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
above book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
test book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
from book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
swap_pair book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
swap_sum book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
to book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
add_comm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
Tuple book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
f book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
reverse_mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
reverse_mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
reverse_mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
reverse_mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
reverse_mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
reverse_mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
reverse_mk_symm book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
f book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
f book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name
g book/TPiL/Tactics.lean trust unknown: Lean has no constant by this name