From a3ecefd41506d915a62ac2ce24b16c92085ed6a3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 25 Jun 2026 13:55:00 -0500 Subject: [PATCH] Rename IterProd instances off the inst* prefix The `inst*` prefix is reserved for compiler-generated instance names; writing it by hand is non-idiomatic. Rename the recursive instances in Spa/Lattice/IterProd.lean to descriptive lowerCamelCase matching the file's `def fixedHeight`: instLattice -> lattice, instDecidableEq -> decidableEq, instFiniteHeight -> finiteHeight. Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Lattice/IterProd.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean index e60a76b..485f77f 100644 --- a/lean/Spa/Lattice/IterProd.lean +++ b/lean/Spa/Lattice/IterProd.lean @@ -13,15 +13,15 @@ namespace IterProd variable {A B : Type u} -instance instLattice [Lattice A] [Lattice B] : +instance lattice [Lattice A] [Lattice B] : ∀ k, Lattice (IterProd A B k) | 0 => inferInstanceAs (Lattice B) - | k + 1 => @Prod.instLattice A (IterProd A B k) _ (instLattice k) + | k + 1 => @Prod.instLattice A (IterProd A B k) _ (lattice k) -instance instDecidableEq [DecidableEq A] [DecidableEq B] : +instance decidableEq [DecidableEq A] [DecidableEq B] : ∀ k, DecidableEq (IterProd A B k) | 0 => inferInstanceAs (DecidableEq B) - | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k) + | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (decidableEq k) def build (a : A) (b : B) : (k : ℕ) → IterProd A B k | 0 => b @@ -32,9 +32,9 @@ variable [Lattice A] [Lattice B] def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] : ∀ k, FiniteHeightLattice (IterProd A B k) | 0 => inferInstanceAs (FiniteHeightLattice B) - | k + 1 => @Spa.prod A (IterProd A B k) _ (instLattice k) _ (fixedHeight k) + | k + 1 => @Spa.prod A (IterProd A B k) _ (lattice k) _ (fixedHeight k) -instance instFiniteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) : +instance finiteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) : FiniteHeightLattice (IterProd A B k) := fixedHeight k theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :