summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-07-17 12:14:03 +0200
committerSon Ho2023-07-17 12:14:03 +0200
commitd45c6ed9e8049b81170c3e6950043d08006ba9f2 (patch)
treeeb15b4cc1d1d175bf7737d1e12442a4df01e0bc1 /backends
parent4f7ebc2358d78d31d63a609a32e5a732b82d468e (diff)
Move a definition
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Arith/Arith.lean3
-rw-r--r--backends/lean/Base/Primitives.lean3
2 files changed, 3 insertions, 3 deletions
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
@@ -16,9 +16,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
forbidden):
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 :=