Merge branch 'main' into heyting

Author: Seasawher

.lycheeignore

@@ -2,3 +2,4 @@ https://raw.githubusercontent.com/lean-ja/lean-by-example/.*
 https://adam.math.hhu.de/#/g/leanprover-community/NNG4
 https://live.lean-lang.org/
 https://reservoir.lean-lang.org/
+https://leansearch.net/

book.toml

@@ -56,5 +56,3 @@ level = 2
 [preprocessor.admonish]
 command = "mdbook-admonish"
 assets_version = "3.0.2" # do not edit: managed by `mdbook-admonish install`
-
-### 注意: PDF 生成時に book-pdf.toml の内容が末尾に自動で追加される ###

lake-manifest.json

@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
+   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
+   "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -81,11 +81,21 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0c4fd28f40011b35f5344cd35e9f2a759fdbe045",
+   "rev": "605d02e962dfeba76e53d102502b0ba1eed614bf",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",