From 35e41dd3b0c6fc65a6a98c909d769a0a8120bd79 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Tue, 31 Oct 2023 21:39:32 -0400
Subject: [PATCH] chore: test patch for std4#203

---
 lake-manifest.json | 16 ++++++++--------
 lakefile.lean      |  2 +-
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 99a5e90a2ebf0e..9b84bc639a5640 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -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",
@@ -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"}
diff --git a/lakefile.lean b/lakefile.lean
index f1b8ef2bae0da8..71113c45a6e932 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -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"