Search results

The "copy to clipboard" functionality duplicates preamble code and removes newlines

Status: Open.

#226 In leanprover/theorem_proving_in_lean4;

· jhrcek opened on Jul 15, 2026

Chapter 8.8 Dependent Pattern Matching claims Vect.tail needs an auxiliary function

Status: Open.

#222 In leanprover/theorem_proving_in_lean4;

· lilyball opened on Jun 7, 2026

Suggestion: provide FP detail in Chapter 3.4 description of suffices

Status: Open.

#219 In leanprover/theorem_proving_in_lean4;

· joelkronqvist opened on May 5, 2026

Chapter 8.6 Functional Induction - unnecessary simp [ack, *]

Status: Open.

#218 In leanprover/theorem_proving_in_lean4;

· alpaylan opened on Apr 5, 2026

Chapter 8.6 Functional Induction - simp ack is unsued

Status: Open.

#215 In leanprover/theorem_proving_in_lean4;

· rubydusa opened on Jan 26, 2026

Axioms and Computation: Incorrect definition of linv and consequently proof of linv_comp_self

Status: Open.

#214 In leanprover/theorem_proving_in_lean4;

· dfpetrin opened on Jan 5, 2026

TPiL/InductiveTypes results in build errors

Status: Open.

#212 In leanprover/theorem_proving_in_lean4;

· h-bex opened on Dec 21, 2025

7.7 Inductive Families: Unknown constant subst.match_1_1

Status: Open.

#209 In leanprover/theorem_proving_in_lean4;

· asiz opened on Dec 5, 2025

[Typo] 7.6. Tactics for Inductive Types: on goal assign variable names -> ???

Status: Open.

#208 In leanprover/theorem_proving_in_lean4;

· asiz opened on Dec 5, 2025

[Grammar] 7.1. Enumerated Types: they construct -> it constructs

Status: Open.

#207 In leanprover/theorem_proving_in_lean4;

· asiz opened on Dec 5, 2025

[Typo] 6.11. Using the Library: name of theorem -> name of the theorem

Status: Open.

#206 In leanprover/theorem_proving_in_lean4;

· asiz opened on Dec 5, 2025

6.1. Messages: swap order of expected error and warning in Docstring

Status: Open.

#205 In leanprover/theorem_proving_in_lean4;

· asiz opened on Dec 5, 2025