`calc` tactic display

[hrmacbeth]

The calc tactic has a slightly distracting Paperproof display which privileges the first line of the calc (printing this explicitly) over the later lines. Term-mode calc does not seem to have this issue.

Example:

import Mathlib.Tactic.Ring
import Paperproof

example {a b : ℕ} (h : b = 2 * a) : ∃ x : ℕ, b ^ 3 + 1 = 2 * x + 1 := by
  have H :=
  -- term-mode `calc`
  calc b ^ 3 + 1 = (2 * a) ^ 3 + 1 := by rw [h]
    _ = 2 * (4 * a ^ 3) + 1 := by ring
  exact ⟨_, H⟩

example {a b : ℕ} (h : b = 2 * a) : ∃ x : ℕ, b ^ 3 + 1 = 2 * x + 1 := by
  use 4 * a ^ 3
  -- tactic-mode `calc`
  calc b ^ 3 + 1 = (2 * a) ^ 3 + 1 := by rw [h]
    _ = 2 * (4 * a ^ 3) + 1 := by ring

Here's the Paperproof output, in order: In the second one (tactic-mode calc) this line is printed:

  calc b ^ 3 + 1 = (2 * a) ^ 3 + 1 := by rw [h]

This line is only part of the full calc, and the later line(s) of the calc don't appear; the asymmetry is a bit confusing. Is there a way to suppress this line from the Paperproof output?

[lakesare]

Thanks for the example!

Technically, we just grab the entire line here. So, one trick to deal with similar issues is to move everything after calc (or any other such tactic) to the new line:

---

Paperproof shouldn't require people to move calc arguments to the new line however. I'll pr the fix, and in the future we'll be fixing such issues in the ad hoc manner. When the current main is deployed, your proof will be rendered as follows:

---

[This issue will be closed once the new version of Paperproof vscode extension is published]

[lakesare]

The vscode extension version that fixes this is v1.6.0, and it's live: https://github.com/Paper-Proof/paperproof/releases/tag/1.6.0.