Skip to content

Commit

Permalink
chore: update to most recent nightly, Std moved to Lean
Browse files Browse the repository at this point in the history
  • Loading branch information
mhuisi committed Sep 28, 2022
1 parent 1f844d9 commit 80b783a
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 7 deletions.
6 changes: 3 additions & 3 deletions Cli/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions Cli/Extensions.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:nightly-2022-09-01
leanprover/lean4:nightly-2022-09-28

0 comments on commit 80b783a

Please sign in to comment.