diff options
Diffstat (limited to 'backends/lean')
| -rw-r--r-- | backends/lean/Base/Arith/Arith.lean | 3 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives.lean | 3 |
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 := |