Skip to content

Fix rw explanation in Tactics chapter#217

Open
freizl wants to merge 1 commit intoleanprover:masterfrom
freizl:master
Open

Fix rw explanation in Tactics chapter#217
freizl wants to merge 1 commit intoleanprover:masterfrom
freizl:master

Conversation

@freizl
Copy link

@freizl freizl commented Feb 24, 2026

For this example

example (a b c : Nat) : a + b + c = a + c + b := by
  rw [Nat.add_assoc, Nat.add_comm b, ← Nat.add_assoc]

This PR fixes a documentation error in the rw tactic explanation in book/TPiL/Tactics.lean.

The text previously said that, without specifying the argument, rewriting
a + (b + c) with Nat.add_comm would produce (b + c) + a.
That is incorrect for this example.

It now correctly states that the rewrite is:
a + (b + c) -> a + (c + b).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant