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


From b3dd78ff4c8785b6ff9bce9927df90f8c78a9109 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 22:04:13 +0200
Subject: Update Lean to v4.9.0-rc1

---
 backends/lean/Base/Primitives/Vec.lean | 3 +--
 1 file changed, 1 insertion(+), 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 d144fcb8..0b010944 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
 import Base.Primitives.ArraySlice
@@ -59,7 +58,7 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
     have h : nlen ≤ Usize.max := by
       simp [Usize.max] at *
       have hm := Usize.refined_max.property
-      cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith
+      cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try omega
     ok ⟨ List.concat v.val x, by simp at *; assumption ⟩
   else
     fail maximumSizeExceeded
-- 
cgit v1.2.3