Skip to content

Commit

Permalink
chore: test patch for std4#203
Browse files Browse the repository at this point in the history
  • Loading branch information
fgdorais committed Nov 1, 2023
1 parent eb40450 commit 35e41dd
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 9 deletions.
16 changes: 8 additions & 8 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,6 @@
"packagesDir": "lake-packages",
"packages":
[{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "a71c160b1934814837d37f377efaf2964e55c433",
"opts": {},
"name": "std",
"inputRev?": "main",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover-community/quote4",
"subDir?": null,
"rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
Expand Down Expand Up @@ -40,5 +32,13 @@
"opts": {},
"name": "proofwidgets",
"inputRev?": "v0.0.21",
"inherited": false}},
{"git":
{"url": "https://github.com/fgdorais/std4",
"subDir?": null,
"rev": "c00d3b184f5df002a18055120fa4032ecec4aad7",
"opts": {},
"name": "std",
"inputRev?": "nat-sub",
"inherited": false}}],
"name": "mathlib"}
2 changes: 1 addition & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ lean_exe checkYaml where
meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

require std from git "https://github.com/leanprover/std4" @ "main"
require std from git "https://github.com/fgdorais/std4" @ "nat-sub"
require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
require Cli from git "https://github.com/leanprover/lean4-cli" @ "nightly"
Expand Down

0 comments on commit 35e41dd

Please sign in to comment.