Search results

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

[Typo] 2.9. Implicit Arguments: The makes -> The braces make

Status: Open.

#204 In leanprover/theorem_proving_in_lean4;

· asiz opened on Dec 5, 2025

7.5 Other Recursive Data Types

Status: Open.

#200 In leanprover/theorem_proving_in_lean4;

· ebotcazou opened on Nov 26, 2025

7.3 Inductively Defined Propositions

Status: Open.

#196 In leanprover/theorem_proving_in_lean4;

· ebotcazou opened on Nov 20, 2025