From b3ebddc119082473cd3dd4afd8ddf5b6517d99cc Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 2 May 2023 09:14:50 -0600 Subject: [PATCH] Add std4 library to bookshelf. --- lake-manifest.json | 6 ++++++ lakefile.lean | 3 +++ 2 files changed, 9 insertions(+) diff --git a/lake-manifest.json b/lake-manifest.json index 0c15284..7a65f57 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -19,6 +19,12 @@ "rev": "071464ac36e339afb7a87640aa1f8121f707a59a", "name": "aesop", "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/leanprover/std4.git", + "subDir?": null, + "rev": "6006307d2ceb8743fea7e00ba0036af8654d0347", + "name": "std4", + "inputRev?": "6006307d2ceb8743fea7e00ba0036af8654d0347"}}, {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 9f8afd4..e8b0cb8 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,6 +6,9 @@ package «bookshelf» require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" +require std4 from git + "https://github.com/leanprover/std4.git" @ + "6006307d2ceb8743fea7e00ba0036af8654d0347" @[default_target] lean_lib «Bookshelf» {