DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Rename IterProd instances off the inst* prefix

Browse Source 
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 <noreply@anthropic.com>
This commit is contained in:
Danila Fedorin
2026-06-25 13:55:00 -05:00
parent 5ac881559d
commit a3ecefd415
1 changed files with 6 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
lean/Spa/Lattice/IterProd.lean
View File

@@ -13,15 +13,15 @@ namespace IterProd
variable {A B : Type u} variable {A B : Type u}
instance instLattice [Lattice A] [Lattice B] : instance lattice [Lattice A] [Lattice B] :
∀ k, Lattice (IterProd A B k) ∀ k, Lattice (IterProd A B k)
| 0 => inferInstanceAs (Lattice B) | 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) ∀ k, DecidableEq (IterProd A B k)
| 0 => inferInstanceAs (DecidableEq B) | 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 def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
| 0 => b | 0 => b
@@ -32,9 +32,9 @@ variable [Lattice A] [Lattice B]
def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] : def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
∀ k, FiniteHeightLattice (IterProd A B k) ∀ k, FiniteHeightLattice (IterProd A B k)
| 0 => inferInstanceAs (FiniteHeightLattice B) | 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 FiniteHeightLattice (IterProd A B k) := fixedHeight k
theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] : theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :