chore: bump to Lean 4 nightly 2021-12-13 (#130)

Author: gebner

Mathlib/Data/ByteArray.lean

@@ -94,13 +94,13 @@ def String.toAsciiByteArray (s : String) : ByteArray :=
 
 /-- Convert a byte slice into a string. This does not handle non-ASCII characters correctly:
 every byte will become a unicode character with codepoint < 256. -/
-def ByteSlice.toString (bs : ByteSlice) : String := do
+def ByteSlice.toString (bs : ByteSlice) : String := Id.run do
   let mut s := ""
   for c in bs do s := s.push c.toChar
   s
 
 instance : ToString ByteSlice where
-  toString bs := do
+  toString bs := Id.run do
     let mut s := ""
     for c in bs do s := s.push c.toChar
     s

Mathlib/Data/List/Defs.lean

@@ -19,15 +19,15 @@ namespace List
 `[f 0 a₀, f 1 a₁, ...]`. -/
 def mapIdx (as : List α) (f : ℕ → α → β) : List β :=
   let rec loop : ℕ → List α → List β
-  | _,  [] => return []
+  | _,  [] => []
   | n, a :: as => f n a :: loop (n + 1) as
   loop 0 as
 
 /-- Applicative variant of `mapWithIndex`. -/
 def mapIdxM {m : Type v → Type w} [Applicative m] (as : List α) (f : ℕ → α → m β) :
   m (List β) :=
   let rec loop : ℕ → List α → m (List β)
-  | _,  [] => return []
+  | _,  [] => []
   | n, a :: as => List.cons <$> f n a <*> loop (n + 1) as
   loop 0 as
 

Mathlib/Lean/Expr.lean

@@ -35,7 +35,7 @@ namespace Name
 
 /-- Find the largest prefix `n` of a `Name` such that `f n != none`, then replace this prefix
 with the value of `f n`. -/
-def mapPrefix (f : Name → Option Name) (n : Name) : Name := do
+def mapPrefix (f : Name → Option Name) (n : Name) : Name := Id.run do
   if let some n' := f n then return n'
   match n with
   | anonymous => anonymous

Mathlib/Mathport/Rename.lean

@@ -23,7 +23,7 @@ initialize renameExtension : SimplePersistentEnvExtension (Name × Name) RenameM
     addImportedFn := fun es => mkStateFromImportedEntries (RenameMap.insertPair) {} es
   }
 
-def getRenameMap (env : Environment) : RenameMap := do
+def getRenameMap (env : Environment) : RenameMap :=
   renameExtension.getState env
 
 def addNameAlignment (n3 n4 : Name) : CoreM Unit := do

Mathlib/Tactic/Lint/Frontend.lean

@@ -47,7 +47,7 @@ omits it from only the specified linter checks.
 sanity check, lint, cleanup, command, tactic
 -/
 
-def Lean.TagAttribute.getDecls (attr : TagAttribute) (env : Environment) : Array Name := do
+def Lean.TagAttribute.getDecls (attr : TagAttribute) (env : Environment) : Array Name := Id.run do
   let st := attr.ext.toEnvExtension.getState env
   let mut decls := st.state.toArray
   for ds in st.importedEntries do

Mathlib/Tactic/Lint/Simp.lean

@@ -7,10 +7,6 @@ import Mathlib.Tactic.Lint.Basic
 import Mathlib.Tactic.OpenPrivate
 open Lean Meta
 
-def Option.mapM [Monad m] (f : α → m β) : Option α → m (Option β)
-  | none => none
-  | some a => f a
-
 namespace Mathlib.Tactic.Lint
 
 /-!

Mathlib/Tactic/OpenPrivate.lean

@@ -38,7 +38,7 @@ def elabOpenPrivateLike (ids : Array Syntax) (tgts mods : Option (Array Syntax))
     for declName in (← getEnv).declsInModuleIdx modIdx do
       if isPrivateName declName then
         names := names.insert declName
-  let appendNames (msg : String) : String := do
+  let appendNames (msg : String) : String := Id.run do
     let mut msg := msg
     for c in names do
       if let some name := privateToUserName? c then
@@ -61,7 +61,7 @@ def elabOpenPrivateLike (ids : Array Syntax) (tgts mods : Option (Array Syntax))
         decls := decls.push (OpenDecl.explicit n new)
       else unreachable!
     | _ => throwError s!"provided name is ambiguous: found {found.map privateToUserName?}"
-  modifyScope fun scope => do
+  modifyScope fun scope => Id.run do
     let mut openDecls := scope.openDecls
     for decl in decls do
       openDecls := decl::openDecls

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2021-12-08
+leanprover/lean4:nightly-2021-12-13