summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon Ho2023-07-17 12:12:34 +0200
committerSon Ho2023-07-17 12:12:34 +0200
commit4f7ebc2358d78d31d63a609a32e5a732b82d468e (patch)
tree0c6d576aec1bd027530877ce24fbef0c99425205 /backends/lean
parenta9a3376443e4c6d9a5257bdd310966a59aa9e716 (diff)
Update the lean dependencies and update IList
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base.lean1
-rw-r--r--backends/lean/Base/IList.lean1
-rw-r--r--backends/lean/Base/Progress/Progress.lean3
-rw-r--r--backends/lean/lake-manifest.json14
-rw-r--r--backends/lean/lean-toolchain2
5 files changed, 12 insertions, 9 deletions
diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
index 51211704..2077d410 100644
--- a/backends/lean/Base.lean
+++ b/backends/lean/Base.lean
@@ -3,3 +3,4 @@ import Base.Primitives
import Base.Diverge
import Base.Arith
import Base.Progress
+import Base.IList
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) :
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index f4759ad3..5a089838 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -8,26 +8,32 @@
"name": "proofwidgets",
"inputRev?": "v0.0.11"}},
{"git":
+ {"url": "https://github.com/mhuisi/lean4-cli.git",
+ "subDir?": null,
+ "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+ "name": "Cli",
+ "inputRev?": "nightly"}},
+ {"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
- "rev": "cc5d11f24e1b92db65ec3389bb5142f4b2d7670e",
+ "rev": "fa05951a270fef2873666c46f138e90338cd48d6",
"name": "mathlib",
"inputRev?": null}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
- "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
+ "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55",
"name": "Qq",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/JLimperg/aesop",
"subDir?": null,
- "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
+ "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
"name": "aesop",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
- "rev": "e68aa8f5fe47aad78987df45f99094afbcb5e936",
+ "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
"name": "std",
"inputRev?": "main"}}]}
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index 42e7d786..334c5053 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-06-20 \ No newline at end of file
+leanprover/lean4:nightly-2023-07-12 \ No newline at end of file