Fix #2462 by removing duplicate infix definition

agda · Aug 20, 2024 · 3e5861c · 3e5861c
1 parent dd7c481
commit 3e5861c
Showing 1 changed file with 0 additions and 2 deletions.
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′)