chore: update toolchain

Mathlib/Tactic/Cases.lean

@@ -57,9 +57,9 @@ def ElimApp.evalNames (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (wit
 
 open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
 elab (name := induction') tk:"induction' " tgts:(casesTarget,+)
-    usingArg:(" using " ident)?
-    withArg:(" with " (colGt binderIdent)+)?
-    genArg:(" generalizing " (colGt ident)+)? : tactic => do
+    usingArg:((" using " ident)?)
+    withArg:((" with " (colGt binderIdent)+)?)
+    genArg:((" generalizing " (colGt ident)+)?) : tactic => do
   let targets ← elabCasesTargets tgts.getSepArgs
   let (elimName, elimInfo) ← getElimNameInfo usingArg targets (induction := true)
   let g ← getMainGoal
@@ -87,8 +87,8 @@ elab (name := induction') tk:"induction' " tgts:(casesTarget,+)
       setGoals (subgoals ++ result.others).toList
 
 open private getElimNameInfo in evalCases in
-elab (name := cases') "cases' " tgts:(casesTarget,+) usingArg:(" using " ident)?
-  withArg:(" with " (colGt binderIdent)+)? : tactic => do
+elab (name := cases') "cases' " tgts:(casesTarget,+) usingArg:((" using " ident)?)
+  withArg:((" with " (colGt binderIdent)+)?) : tactic => do
   let targets ← elabCasesTargets tgts.getSepArgs
   let (elimName, elimInfo) ← getElimNameInfo usingArg targets (induction := false)
   let g ← getMainGoal

Mathlib/Tactic/Have.lean

@@ -49,7 +49,7 @@ def haveLetCore (mvarId : MVarId) (name : Option Syntax) (bis : Array Syntax)
     let (fvar, mvar2) ← intro1P (← declFn mvarId n t p)
     if let some stx := name then
       withMVarContext mvar2 do
-        Term.addTermInfo (isBinder := true) stx (mkFVar fvar)
+        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar)
     pure (mvar1, mvar2)
 
 elab_rules : tactic

Mathlib/Tactic/Lint/Frontend.lean

@@ -186,19 +186,19 @@ elab "#lint"
     fast:"*"?
     only:(&"only")? linters:(ident)*
     : command => do
-  let (decls, whereDesc, groupByFilename) ← match project.getOptional? with
+  let (decls, whereDesc, groupByFilename) ← match project with
     | none => do pure (← liftCoreM getDeclsInCurrModule, "in the current file", false)
     | some (Syntax.atom _ "mathlib") => do pure (← liftCoreM getDeclsInMathlib, "in mathlib", true)
     | some (Syntax.atom _ "all") => do pure (← liftCoreM getAllDecls, "in all files", true)
     | _ => throwUnsupportedSyntax
-  let verbosity : LintVerbosity ← match verbosity.getOptional? with
+  let verbosity : LintVerbosity ← match verbosity with
     | none => pure LintVerbosity.medium
     | some (Syntax.atom _ "+") => pure LintVerbosity.high
     | some (Syntax.atom _ "-") => pure LintVerbosity.low
     | _ => throwUnsupportedSyntax
-  let fast := fast.getOptional?.isSome
-  let only := only.getOptional?.isSome
-  let extraLinters ← linters.getArgs.mapM fun id =>
+  let fast := fast.isSome
+  let only := only.isSome
+  let extraLinters ← linters.mapM fun id =>
     withScope ({ · with currNamespace := `Mathlib.Tactic.Lint }) <|
       resolveGlobalConstNoOverload id
   let linters ← liftCoreM <| getChecks (slow := !fast) extraLinters.toList only

Mathlib/Tactic/NormCast/Tactic.lean

@@ -200,9 +200,9 @@ def normCastHyp (fvarId : FVarId) : TacticM Unit :=
   liftMetaTactic1 fun mvarId => do
     let hyp ← instantiateMVars (← getLocalDecl fvarId).type
     let prf ← derive hyp
-    return (← applySimpResultToLocalDecl mvarId fvarId prf).map (·.snd)
+    return (← applySimpResultToLocalDecl mvarId fvarId prf false).map (·.snd)
 
-elab "norm_cast0" loc:(ppSpace location)? : tactic =>
+elab "norm_cast0" loc:((ppSpace location)?) : tactic =>
   withMainContext do
     match expandOptLocation loc with
     | Location.targets hyps target =>
@@ -220,7 +220,6 @@ macro "assumption_mod_cast" : tactic => `(norm_cast0 at * <;> assumption)
 Normalize casts at the given locations by moving them "upwards".
 -/
 macro "norm_cast" loc:(ppSpace location)? : tactic =>
-  let loc := loc.getOptional?
   `(tactic| norm_cast0 $[$loc:location]? <;> try trivial)
 
 /--

Mathlib/Tactic/RCases.lean

@@ -485,7 +485,7 @@ open Elab Elab.Tactic Meta RCases
 elab (name := rcases?) "rcases?" tgts:casesTarget,* num:(" : " num)? : tactic =>
   throwError "unimplemented"
 
-elab (name := rcases) tk:"rcases" tgts:casesTarget,* pat:(" with " rcasesPatLo)? : tactic => do
+elab (name := rcases) tk:"rcases" tgts:casesTarget,* pat:((" with " rcasesPatLo)?) : tactic => do
   let pat ← match pat.getArgs with
   | #[_, pat] => RCasesPatt.parse pat
   | #[] => pure $ RCasesPatt.tuple tk []
@@ -496,8 +496,8 @@ elab (name := rcases) tk:"rcases" tgts:casesTarget,* pat:(" with " rcasesPatLo)?
     replaceMainGoal (← RCases.rcases tgts pat (← getMainGoal))
 
 elab (name := obtain) tk:"obtain"
-    pat:(ppSpace rcasesPatMed)? ty:(" : " term)? val:(" := " term,+)? : tactic => do
-  let pat ← liftM $ pat.getOptional?.mapM RCasesPatt.parse
+    pat:(ppSpace rcasesPatMed)? ty:((" : " term)?) val:((" := " term,+)?) : tactic => do
+  let pat ← liftM $ pat.mapM RCasesPatt.parse
   if val.isNone then
     if ty.isNone then throwError
         ("`obtain` requires either an expected type or a value.\n" ++
@@ -515,7 +515,7 @@ elab (name := obtain) tk:"obtain"
 elab (name := rintro?) "rintro?" (" : " num)? : tactic =>
   throwError "unimplemented"
 
-elab (name := rintro) "rintro" pats:(ppSpace colGt rintroPat)+ ty:(" : " term)? : tactic => do
+elab (name := rintro) "rintro" pats:(ppSpace colGt rintroPat)+ ty:((" : " term)?) : tactic => do
   let ty? := if ty.isNone then none else some ty[1]
   withMainContext do
-    replaceMainGoal (← RCases.rintro ty pats.getArgs ty? (← getMainGoal))
+    replaceMainGoal (← RCases.rintro ty pats ty? (← getMainGoal))

Mathlib/Tactic/Ring.lean

@@ -114,7 +114,7 @@ def pp : HornerExpr → MetaM Format
 | (xadd e a x (_, n) b) => do
   let pa ← a.pp
   let pb ← b.pp
-  let px ← PrettyPrinter.ppExpr Name.anonymous [] x.1
+  let px ← PrettyPrinter.ppExpr x.1
   return "(" ++ pa ++ ") * (" ++ px ++ ")^" ++ toString n ++ " + " ++ pb
 
 end HornerExpr

Mathlib/Tactic/Sat/FromLRAT.lean

@@ -607,7 +607,7 @@ elab "lrat_proof" n:(ident <|> "example") cnf:term:max lrat:term:max : command =
     let go := do
       fromLRAT cnf lrat name
       withSaveInfoContext do
-        Term.addTermInfo n (mkConst name) (isBinder := true)
+        Term.addTermInfo' n (mkConst name) (isBinder := true)
     if n.isIdent then go else withoutModifyingEnv go
 
 lrat_proof example

Mathlib/Tactic/Set.lean

@@ -49,7 +49,7 @@ elab_rules : tactic
       let (fvar, mvarId) ← intro1P (← define mvarId a.getId ty val)
       pure (fvar, [mvarId])
     withMainContext do
-      Term.addTermInfo (isBinder := true) a (mkFVar fvar)
+      Term.addTermInfo' (isBinder := true) a (mkFVar fvar)
   if rw.isNone then
     evalTactic (← `(tactic| try rewrite [(id rfl : $val = $a)] at *))
   match h, rev with

Mathlib/Tactic/SimpRw.lean

@@ -33,7 +33,6 @@ by simp_rw [h1, h2]
 ```
 -/
 macro "simp_rw " rws:rwRuleSeq loc:(ppSpace location)? : tactic => do
-  let loc := loc.getOptional?
   let stx ← rws[1].getSepArgs.mapM fun
     | `(rwRule| $e:term) => `(tactic| simp%$e only [$e:term] $(loc)?)
     | `(rwRule| ←%$tk $e:term) => `(tactic| simp%$tk only [← $e:term] $(loc)?)

Mathlib/Tactic/TryThis.lean

@@ -28,8 +28,7 @@ partial def replaceMVarsByUnderscores [Monad m] [MonadQuotation m]
     pure s
 
 def delabToRefinableSyntax (e : Expr) : TermElabM Syntax := do
-  let stx ← delab (← readThe Core.Context).currNamespace
-    (← readThe Core.Context).openDecls e
+  let stx ← delab e
   replaceMVarsByUnderscores stx
 
 def addSuggestion [Monad m] [MonadLog m] [AddMessageContext m]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-04-04
+leanprover/lean4:nightly-2022-04-16