From 1259db13a154b0d5f101d2f874ae017b81ed4e72 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 22:54:52 +0100
Subject: Fix more proofs

---
 backends/lean/Base/Primitives/Vec.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 12733a34..b03de15b 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -35,7 +35,7 @@ abbrev Vec.v {α : Type u} (v : Vec α) : List α := v.val
 example {a: Type u} (v : Vec a) : v.length ≤ Scalar.max ScalarTy.Usize := by
   scalar_tac
 
-def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
+def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp; decide ⟩
 
 instance (α : Type u) : Inhabited (Vec α) := by
   constructor
-- 
cgit v1.2.3

