chore: update toolchain

Http/HeaderName.lean

@@ -4,7 +4,7 @@
 -/
 
 import Lean
-import Std
+import Batteries
 import Qq
 import Http.CaseInsString
 import Http.Std

Http/Headers.lean

@@ -3,7 +3,7 @@
     Authors: James Gallicchio
 -/
 
-import Std
+import Batteries
 import Http.Parser
 import Http.HeaderName
 
@@ -27,7 +27,7 @@ def toRequestFormat (h : Headers) : String :=
 def empty : Headers := .empty
 
 def add (self : Headers) (name : HeaderName) (value : String) : Headers :=
-  match self.find? name with
+  match self.get? name with
   | none => self.insert name [value]
   | some v => self.insert name (value :: v)
 

Http/Parser.lean

@@ -14,7 +14,7 @@ def Parser.capture (p : Parser α) : Parser Substring := do
   let p1 ← Parser.getPosition
   let _ ← p
   let p2 ← Parser.getPosition
-  return { (← StateT.get).stream with
+  return { ← Parser.getStream with
       startPos := p1
       stopPos := p2
     }

Http/Status.lean

@@ -4,7 +4,7 @@
 -/
 
 import Lean
-import Std
+import Batteries
 import Qq
 import Http.Std
 import Http.Parser

Http/Std.lean

@@ -4,7 +4,7 @@
 -/
 
 import Lean
-import Std
+import Batteries
 
 def Lean.mkDocComment (s : String) :=
   mkNode ``Parser.Command.docComment #[mkAtom "/--", mkAtom (s ++ "-/")]

Http/URI.lean

@@ -4,7 +4,7 @@
 -/
 
 import Lean
-import Std
+import Batteries
 import Http.Parser
 import Http.CaseInsString
 
@@ -31,7 +31,7 @@ def ofString (s : String) : Option Scheme :=
   else
     none
 
-instance : Inhabited Scheme := ⟨ofString "a" |>.get rfl⟩
+instance : Inhabited Scheme := ⟨ofString "a" |>.get (by with_unfolding_all rfl)⟩
 
 def HTTP := ofString "http" |>.get!
 def HTTPS := ofString "https" |>.get!

lake-manifest.json

@@ -1,41 +1,45 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/gebner/quote4",
+ [{"url": "https://github.com/fgdorais/lean4-parser",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
-   "name": "Qq",
+   "scope": "",
+   "rev": "15c281a401adacf37f406aa24238d412188834fd",
+   "name": "Parser",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/std4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "b1ebd72c5d262ea10a33ea582525925df874ad1e",
-   "name": "std",
+   "scope": "",
+   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/gebner/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "8603bb1d0d5edae780e3a85a0398fd83dbbb80a3",
-   "name": "UnicodeBasic",
+   "scope": "",
+   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
+   "inputRev": "master",
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-parser",
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "e13af0e4538b2dbcb9f3b35e73126c36019a06bd",
-   "name": "Parser",
+   "scope": "",
+   "rev": "470c41643209208d325a5a7315116f293c7443fb",
+   "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
-   "inherited": false,
+   "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "Http",
  "lakeDir": ".lake"}

lakefile.lean

@@ -7,5 +7,5 @@ package Http
 lean_lib Http
 
 require Qq from git "https://github.com/gebner/quote4" @ "master"
-require std from git "https://github.com/leanprover/std4" @ "main"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "main"
 require Parser from git "https://github.com/fgdorais/lean4-parser" @ "main"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.15.0-rc1