Paperproof v1.7.0

Overview

Changes that make working on real formalization projects with Paperproof easier.

• only show spawned by boxes when we are working on them

  Suppose we have a tactic apply (le_mul_inv_iff₀ (by positivity)).mpr, as seen below.
  This tactic has a "spawned goal" 0 < 2 ^ (100 * a), a goal that we're proving in the by positivity block.
  Previously, we were showing these spawned goals as normal subgoals (left picture).
  Now we're hiding them (right picture), and only showing them when our cursor is directly in that by positivity block.

  BEFORE	NOW

  This is generally good UX for proofs of any size, but it's particularly important in real formalization projects, makes large proofs a lot more readable.

• preliminary implementation of hide/show buttons for have boxes

  On this image, you can see ⛶ and ▬ buttons.
  ⛶ expands the (collapsed) box, ▬ collapses the (expanded) box

  

  This UI needs to be worked on (for example, nothing should move when we click these buttons!), but it's sure better than the collapsing logic we had before.

• hide hypotheses with ✝ in the name
  When we do rcases h with ⟨h1, _⟩, Lean will give us h1 : J ∈ 𝓙 (t.𝔖₀ u₁ u₂) and right✝ : J ∈ Iic (𝓘 u₁).
  From now on, we assume the user used _ because they are not interested in seeing right✝ : J ∈ Iic (𝓘 u₁) , and so we hide ✝-ed hypotheses.