diff options
| author | Son Ho | 2023-07-17 12:12:34 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-17 12:12:34 +0200 |
| commit | 4f7ebc2358d78d31d63a609a32e5a732b82d468e (patch) | |
| tree | 0c6d576aec1bd027530877ce24fbef0c99425205 /backends/lean/Base | |
| parent | a9a3376443e4c6d9a5257bdd310966a59aa9e716 (diff) | |
Update the lean dependencies and update IList
Diffstat (limited to 'backends/lean/Base')
| -rw-r--r-- | backends/lean/Base/IList.lean | 1 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 3 |
2 files changed, 0 insertions, 4 deletions
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) : |