From d45c6ed9e8049b81170c3e6950043d08006ba9f2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 12:14:03 +0200
Subject: Move a definition

---
 backends/lean/Base/Arith/Arith.lean | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'backends/lean/Base/Arith')

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 8bfad6ae..da263e86 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -15,9 +15,6 @@ namespace Arith
 
 open Primitives Utils
 
--- TODO: move
-instance Vec.cast (a : Type): Coe (Vec a) (List a)  where coe := λ v => v.val
-
 -- TODO: move
 /- Remark: we can't write the following instance because of restrictions about
    the type class parameters (`ty` doesn't appear in the return type, which is
-- 
cgit v1.2.3