Commit 2023-10-20 16:10 b8e9a283

View on Github →

fix(says tactic): Don’t stumble over Try this:\n instead of Try this:␣ (#7803) as discussed in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Lake.20build.20succeeds.20on.20local.2C.20but.20fails.20on.20GitHub.20Action/near/397679705

Estimated changes

Modified Mathlib/Tactic/Says.lean

Modified test/says.lean

added def P

added def Q

added def very_long_lemma_name_aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

added def very_long_lemma_name_bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb