From 10bccfe501ce08ecb23511bb014292ebe6595db4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 6 Mar 2022 13:58:42 -0800
Subject: [PATCH] test: remove workaround

---
 tests/lean/run/interp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/interp.lean b/tests/lean/run/interp.lean
index e2cd73a612..41e4a4e115 100644
--- a/tests/lean/run/interp.lean
+++ b/tests/lean/run/interp.lean
@@ -2,7 +2,7 @@ inductive Vector (α : Type u) : Nat → Type u
   | nil : Vector α 0
   | cons : α → Vector α n → Vector α (n+1)
 
-infix:67 (priority := high) " :: " => Vector.cons
+infix:67 " :: " => Vector.cons
 
 inductive Ty where
   | int