consistent equation spacing (#457)

Most declarations that use the keyword `equation` have two spaces on each side of `:=` so I put it everywhere consistently.
teorth · Oct 9, 2024 · 2a5b2f0 · 2a5b2f0
1 parent ba6490a
commit 2a5b2f0
Showing 1 changed file with 14 additions and 14 deletions.
diff --git a/equational_theories/Equations.lean b/equational_theories/Equations.lean
@@ -13,45 +13,45 @@ The equations are marked as `abbrev` so that tactics like `decide` will look thr
 -/
 
 /-- The reflexive law -/
-equation 1 := x = x
+equation 1  :=  x = x
 
 /-- The singleton law -/
-equation 2  := x = y
+equation 2  :=  x = y
 
 /-- The idempotence law -/
-equation 3  := x = x ◇ x
+equation 3  :=  x = x ◇ x
 
 /-- The left absorption law -/
-equation 4  := x = x ◇ y
+equation 4  :=  x = x ◇ y
 
 /-- The right absorption law -/
-equation 5  := x = y ◇ x
+equation 5  :=  x = y ◇ x
 
 @[inherit_doc Equation2]
-equation 6  := x = y ◇ y
+equation 6  :=  x = y ◇ y
 
 @[inherit_doc Equation2]
-equation 7  := x = y ◇ z
+equation 7  :=  x = y ◇ z
 
 /-- dual of 23 -/
-equation 8  := x = x ◇ (x ◇ x)
+equation 8  :=  x = x ◇ (x ◇ x)
 
 /-- Appears in Problem A1 from Putnam 2001 -/
-equation 14  := x = y ◇ (x ◇ y)
+equation 14  :=  x = y ◇ (x ◇ y)
 
-equation 16  := x = y ◇ (y ◇ x)
+equation 16  :=  x = y ◇ (y ◇ x)
 
 /-- dual of 8 -/
-equation 23  := x = (x ◇ x) ◇ x
+equation 23  :=  x = (x ◇ x) ◇ x
 
 /-- Appears in Problem A1 from Putnam 2001.  Dual of 14 -/
-equation 29  := x = (y ◇ x) ◇ y
+equation 29  :=  x = (y ◇ x) ◇ y
 
 /-- value of multiplication is independent of right argument -/
-equation 38  := x ◇ x = x ◇ y
+equation 38  :=  x ◇ x = x ◇ y
 
 /-- value of multiplication is independent of left argument; dual of 38 -/
-equation 39  := x ◇ x = y ◇ x
+equation 39  :=  x ◇ x = y ◇ x
 
 /-- all squares are the same -/
 equation 40  :=  x ◇ x = y ◇ y