From 4f7ebc2358d78d31d63a609a32e5a732b82d468e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 12:12:34 +0200
Subject: Update the lean dependencies and update IList

---
 backends/lean/Base/IList.lean             | 1 -
 backends/lean/Base/Progress/Progress.lean | 3 ---
 2 files changed, 4 deletions(-)

(limited to 'backends/lean/Base')

diff --git a/backends/lean/Base/IList.lean b/backends/lean/Base/IList.lean
index 7e764d63..3db00cbb 100644
--- a/backends/lean/Base/IList.lean
+++ b/backends/lean/Base/IList.lean
@@ -7,7 +7,6 @@ import Base.Arith
 
 namespace List
 
-#check List.get
 def len (ls : List α) : Int :=
   match ls with
   | [] => 0
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 835dc468..35a3c25a 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -15,7 +15,6 @@ namespace Test
   @[pspec]
   theorem vec_index_test (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
     ∃ x, v.index α i = .ret x := by
-      apply
       sorry
 
   #eval pspecAttr.find? ``Primitives.Vec.index
@@ -195,7 +194,6 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
       args.map Syntax.getId
     else #[]
   trace[Progress] "Ids: {ids}"
-  --if args[0] ≠ some "as" then throwError "Invalid syntax: should be: `progress as ⟨ ... ⟩`"
   progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
@@ -205,7 +203,6 @@ namespace Test
   open Primitives
 
   set_option trace.Progress true
-  set_option pp.rawOnError true
 
   @[pspec]
   theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
-- 
cgit v1.2.3