From 80b783a8905a4e8a29ced841abb64f710bc86f06 Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Wed, 28 Sep 2022 18:55:07 +0200
Subject: [PATCH] chore: update to most recent nightly, Std moved to Lean

---
 Cli/Basic.lean      | 6 +++---
 Cli/Extensions.lean | 6 +++---
 lean-toolchain      | 2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Cli/Basic.lean b/Cli/Basic.lean
index 0bc6b16..8f3e8cd 100644
--- a/Cli/Basic.lean
+++ b/Cli/Basic.lean
@@ -943,7 +943,7 @@ section Configuration
     /-- Converts `c` back into a `Cli.Cmd`, using the extensions denoted in `original`. -/
     partial def toFullCmd (c : ExtendableCmd) (original : Cli.Cmd) : Cli.Cmd := Id.run do
       let extensions := collectExtensions original
-      let mut extensionIndex := Std.mkRBMap String (Option Extension) compare
+      let mut extensionIndex := Lean.mkRBMap String (Option Extension) compare
       for ⟨fullName, extension?⟩ in extensions do
         extensionIndex := extensionIndex.insert fullName extension?
       let rec loop (c : ExtendableCmd) : Cli.Cmd :=
@@ -1358,14 +1358,14 @@ section Parsing
     private partial def readMultiFlag? : ParseM (Option (Array Parsed.Flag)) := do
       let some (flagContent, true) ← readFlagContent?
         | return none
-      let some (parsedFlags : Array (String × Parsed.Flag)) ← loop flagContent Std.RBTree.empty
+      let some (parsedFlags : Array (String × Parsed.Flag)) ← loop flagContent Lean.RBTree.empty
         | return none
       for (inputFlagName, parsedFlag) in parsedFlags do
         ensureFlagUnique parsedFlag.flag ⟨inputFlagName, true⟩
       skip
       return some <| parsedFlags.map (·.2)
     where
-      loop (flagContent : String) (matched : Std.RBTree String compare)
+      loop (flagContent : String) (matched : Lean.RBTree String compare)
         : ParseM (Option (Array (String × Parsed.Flag))) := do
         -- this is not tail recursive, but that's fine: `loop` will only recurse further if the corresponding
         -- flag has not been matched yet, meaning that this can only overflow if the application has an
diff --git a/Cli/Extensions.lean b/Cli/Extensions.lean
index 5b78f3b..adaee30 100644
--- a/Cli/Extensions.lean
+++ b/Cli/Extensions.lean
@@ -8,7 +8,7 @@ section Utils
     -/
     def leftUnionBy [Ord α] (key : β → α) (left : Array β) (right : Array β)
       : Array β := Id.run do
-      let leftMap := left.map (fun v => (key v, v)) |>.toList |> Std.RBMap.ofList (cmp := compare)
+      let leftMap := left.map (fun v => (key v, v)) |>.toList |> Lean.RBMap.ofList (cmp := compare)
       let mut result := left
       for v in right do
         if ¬ leftMap.contains (key v) then
@@ -21,7 +21,7 @@ section Utils
     -/
     def rightUnionBy [Ord α] (key : β → α) (left : Array β) (right : Array β)
       : Array β := Id.run do
-      let rightMap := right.map (fun v => (key v, v)) |>.toList |> Std.RBMap.ofList (cmp := compare)
+      let rightMap := right.map (fun v => (key v, v)) |>.toList |> Lean.RBMap.ofList (cmp := compare)
       let mut result := right
       for v in left.reverse do
         if ¬ rightMap.contains (key v) then
@@ -31,7 +31,7 @@ section Utils
     /-- Deletes all elements from `left` whose `key` is in `right`. -/
     def diffBy [Ord α] (key : β → α) (left : Array β) (right : Array α)
       : Array β :=
-      let rightMap := Std.RBTree.ofList (cmp := compare) right.toList
+      let rightMap := Lean.RBTree.ofList (cmp := compare) right.toList
       left.filter fun v => ¬ (rightMap.contains <| key v)
   end Array
 end Utils
diff --git a/lean-toolchain b/lean-toolchain
index 79f718a..886ada6 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-09-01
+leanprover/lean4:nightly-2022-09-28