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 ---
 backends/lean/Base/Primitives.lean  | 3 +++
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'backends/lean/Base')

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
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 0506f4c0..1a0c665d 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -616,6 +616,9 @@ def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val
 
 def Vec (α : Type u) := { l : List α // List.length l ≤ Usize.max }
 
+-- TODO: do we really need it? It should be with Subtype by default
+instance Vec.cast (a : Type): Coe (Vec a) (List a)  where coe := λ v => v.val
+
 def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
 
 def Vec.len (α : Type u) (v : Vec α) : Usize :=
-- 
cgit v1.2.3