From 3e5861c5a200b26f4254645f1b4921692f0ddcf9 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Tue, 20 Aug 2024 19:58:22 +0800
Subject: [PATCH] Fix #2462 by removing duplicate infix definition

---
 src/Reflection/AST/Definition.agda | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 2671e6241a..dab8ab2505 100644
--- 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′)