From 1979d72b37d3a4abdff555da3f75ecfc9f629c26 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 11:33:13 +0200
Subject: Fix more issues

---
 backends/lean/Base/Primitives/Vec.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(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 5ed7b606..d144fcb8 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -34,7 +34,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; decide ⟩
+def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
 
 instance (α : Type u) : Inhabited (Vec α) := by
   constructor
@@ -192,7 +192,7 @@ def alloc.slice.Slice.to_vec
 def core.slice.Slice.reverse (T : Type) (s : Slice T) : Slice T :=
   ⟨ s.val.reverse, by sorry ⟩
 
-def alloc.vec.Vec.with_capacity (T : Type) (s : Usize) : alloc.vec.Vec T := Vec.new T
+def alloc.vec.Vec.with_capacity (T : Type) (_ : Usize) : alloc.vec.Vec T := Vec.new T
 
 /- [alloc::vec::{(core::ops::deref::Deref for alloc::vec::Vec<T, A>)#9}::deref]:
    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2624:4-2624:27
-- 
cgit v1.2.3