fix: layout of records

jamesmckinna · jamesmckinna · commit e32165092b67 · 2025-11-07T06:38:48.000Z
diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda
@@ -98,7 +98,10 @@ private
         ; injective = id
         }
       }
-    ; isNormal = record { conjugate = const ; normal = commutes }
+    ; isNormal = record
+      { conjugate = const
+      ; normal = commutes
+      }
     }
 
 

Original file line number	Diff line number	Diff line change
`@@ -98,7 +98,10 @@ private`
`98`	`98`	`; injective = id`
`99`	`99`	`}`
`100`	`100`	`}`
`101`		`- ; isNormal = record { conjugate = const ; normal = commutes }`
	`101`	`+ ; isNormal = record`
	`102`	`+ { conjugate = const`
	`103`	`+ ; normal = commutes`
	`104`	`+ }`
`102`	`105`	`}`
`103`	`106`
`104`	`107`