From 5c9c8ac55ce0f8d3731f6c1f1dc0d52d3c073d0e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 25 Jun 2026 13:56:44 -0500 Subject: [PATCH] Fix formatting nits in Lattice.lean and Unit.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Spa/Lattice.lean: add the missing space in the PointedLTSeries binder list ((f t : α) (n : ℕ)). - Spa/Lattice/Unit.lean: use rfl instead of refl _, and split the ~200-column longestChain record literal across lines, one field per line. Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Lattice.lean | 2 +- lean/Spa/Lattice/Unit.lean | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean index d50c8fa..3957f4a 100644 --- a/lean/Spa/Lattice.lean +++ b/lean/Spa/Lattice.lean @@ -50,7 +50,7 @@ end Folds def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop := ∀ c : LTSeries α, c.length ≤ n -structure PointedLTSeries (α : Type*) (f t : α)(n : ℕ) [Preorder α] where +structure PointedLTSeries (α : Type*) (f t : α) (n : ℕ) [Preorder α] where series : LTSeries α head_series : series.head = f last_series : series.last = t diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean index 5959fba..a5763f6 100644 --- a/lean/Spa/Lattice/Unit.lean +++ b/lean/Spa/Lattice/Unit.lean @@ -12,7 +12,11 @@ instance : FiniteHeightLattice PUnit where bot := PUnit.unit top := PUnit.unit height := 0 - longestChain := { series := RelSeries.singleton _ PUnit.unit, head_series := refl _, last_series := refl _, length_series := refl _ } + longestChain := + { series := RelSeries.singleton _ PUnit.unit + head_series := rfl + last_series := rfl + length_series := rfl } chains_bounded := boundedChains_of_subsingleton PUnit 0 end Spa