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/Primitives.lean | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'backends/lean/Base/Primitives.lean')

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