Fix #2462 by removing duplicate infix definition

MatthewDaggitt · MatthewDaggitt · commit 3e5861c5a200 · 2024-08-20T19:58:33.000+08:00
diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
@@ -68,8 +68,6 @@ constructor′-injective = < constructor′-injective₁ , constructor′-inject
 
 infix 4 _≟_
 
-infix 4 _≟_
-
 _≟_ : DecidableEquality Definition
 function cs       ≟ function cs′        =
   map′ (cong function) function-injective (cs Term.≟-Clauses cs′)
