chore: update to nightly-2022-07-28 (#357)

Changed all names related to leanprover/lean4#1346 that I could find.

- [x] leanprover/lean4#1375

Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: Vtec234

Mathlib/Init/ExtendedBinder.lean

@@ -12,7 +12,7 @@ Defines an extended binder syntax supporting `∀ ε > 0, ...` etc.
 
 namespace Mathlib.ExtendedBinder
 
-/-
+/--
 The syntax category of binder predicates contains predicates like `> 0`, `∈ s`, etc.
 (`: t` should not be a binder predicate because it would clash with the built-in syntax for ∀/∃.)
 -/

Mathlib/Lean/NameMapAttribute.lean

@@ -59,7 +59,7 @@ def registerNameMapAttribute (impl : NameMapAttributeImpl α) : IO (NameMapAttri
   registerBuiltinAttribute {
     name := impl.name
     descr := impl.descr
-    add := fun src stx kind => do
+    add := fun src stx _kind => do
       let a : α ← impl.add src stx
       ext.add src a
   }

Mathlib/Tactic/Basic.lean

@@ -119,7 +119,7 @@ where
     | _ => pure ()
   intro1PStep : TacticM Unit :=
     liftMetaTactic fun mvarId => do
-      let (_, mvarId) ← Meta.intro1P mvarId
+      let (_, mvarId) ← mvarId.intro1P
       pure [mvarId]
 
 /-- Try calling `assumption` on all goals; succeeds if it closes at least one goal. -/
@@ -242,7 +242,7 @@ elab "any_goals " seq:tacticSeq : tactic => do
   let mut mvarIdsNew := #[]
   let mut anySuccess := false
   for mvarId in mvarIds do
-    unless (← isExprMVarAssigned mvarId) do
+    unless (← mvarId.isAssigned) do
       setGoals [mvarId]
       try
         evalTactic seq
@@ -255,10 +255,10 @@ elab "any_goals " seq:tacticSeq : tactic => do
   setGoals mvarIdsNew.toList
 
 elab "fapply " e:term : tactic =>
-  evalApplyLikeTactic (Meta.apply (cfg := {newGoals := ApplyNewGoals.all})) e
+  evalApplyLikeTactic (MVarId.apply (cfg := {newGoals := ApplyNewGoals.all})) e
 
 elab "eapply " e:term : tactic =>
-  evalApplyLikeTactic (Meta.apply (cfg := {newGoals := ApplyNewGoals.nonDependentOnly})) e
+  evalApplyLikeTactic (MVarId.apply (cfg := {newGoals := ApplyNewGoals.nonDependentOnly})) e
 
 /--
 Tries to solve the goal using a canonical proof of `True`, or the `rfl` tactic.
@@ -272,5 +272,5 @@ elab (name := clearAuxDecl) "clear_aux_decl" : tactic => withMainContext do
   let mut g ← getMainGoal
   for ldec in ← getLCtx do
     if ldec.isAuxDecl then
-      g ← Meta.tryClear g ldec.fvarId
+      g ← g.tryClear ldec.fvarId
   replaceMainGoal [g]

Mathlib/Tactic/Cases.lean

@@ -48,10 +48,10 @@ def ElimApp.evalNames (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (wit
     let numFields ← getAltNumFields elimInfo altName
     let (altVarNames, names') := names.splitAtD numFields `_
     names := names'
-    let (_, g) ← introN g numFields altVarNames
+    let (_, g) ← g.introN numFields altVarNames
     let some (g, _) ← Cases.unifyEqs? numEqs g {} | pure ()
-    let (_, g) ← introNP g numGeneralized
-    let g ← liftM $ toClear.foldlM tryClear g
+    let (_, g) ← g.introNP numGeneralized
+    let g ← liftM $ toClear.foldlM MVarId.tryClear g
     subgoals := subgoals.push g
   pure subgoals
 
@@ -62,12 +62,12 @@ elab (name := induction') "induction' " tgts:(casesTarget,+)
     genArg:((" generalizing " (colGt ident)+)?) : tactic => do
   let targets ← elabCasesTargets tgts.1.getSepArgs
   let g ← getMainGoal
-  withMVarContext g do
+  g.withContext do
     let elimInfo ← getElimNameInfo usingArg targets (induction := true)
     let targets ← addImplicitTargets elimInfo targets
     evalInduction.checkTargets targets
     let targetFVarIds := targets.map (·.fvarId!)
-    withMVarContext g do
+    g.withContext do
       let genArgs ← if genArg.1.isNone then pure #[] else getFVarIds genArg.1[1].getArgs
       let forbidden ← mkGeneralizationForbiddenSet targets
       let mut s ← getFVarSetToGeneralize targets forbidden
@@ -77,11 +77,11 @@ elab (name := induction') "induction' " tgts:(casesTarget,+)
         if s.contains v then
           throwError "unnecessary 'generalizing' argument, variable '{mkFVar v}' is generalized automatically"
         s := s.insert v
-      let (fvarIds, g) ← Meta.revert g (← sortFVarIds s.toArray)
-      let result ← withRef tgts <| ElimApp.mkElimApp elimInfo targets (← getMVarTag g)
+      let (fvarIds, g) ← g.revert (← sortFVarIds s.toArray)
+      let result ← withRef tgts <| ElimApp.mkElimApp elimInfo targets (← g.getTag)
       let elimArgs := result.elimApp.getAppArgs
       ElimApp.setMotiveArg g elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds
-      assignExprMVar g result.elimApp
+      g.assign result.elimApp
       let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
         (numGeneralized := fvarIds.size) (toClear := targetFVarIds)
       setGoals (subgoals ++ result.others).toList
@@ -91,18 +91,18 @@ elab (name := cases') "cases' " tgts:(casesTarget,+) usingArg:((" using " ident)
   withArg:((" with " (colGt binderIdent)+)?) : tactic => do
   let targets ← elabCasesTargets tgts.1.getSepArgs
   let g ← getMainGoal
-  withMVarContext g do
+  g.withContext do
     let elimInfo ← getElimNameInfo usingArg targets (induction := false)
     let targets ← addImplicitTargets elimInfo targets
-    let result ← withRef tgts <| ElimApp.mkElimApp elimInfo targets (← getMVarTag g)
+    let result ← withRef tgts <| ElimApp.mkElimApp elimInfo targets (← g.getTag)
     let elimArgs := result.elimApp.getAppArgs
     let targets ← elimInfo.targetsPos.mapM (instantiateMVars elimArgs[·]!)
     let motive := elimArgs[elimInfo.motivePos]!
     let g ← generalizeTargetsEq g (← inferType motive) targets
-    let (targetsNew, g) ← introN g targets.size
-    withMVarContext g do
+    let (targetsNew, g) ← g.introN targets.size
+    g.withContext do
       ElimApp.setMotiveArg g motive.mvarId! targetsNew
-      assignExprMVar g result.elimApp
+      g.assign result.elimApp
       let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
          (numEqs := targets.size) (toClear := targetsNew)
       setGoals subgoals.toList

Mathlib/Tactic/Clear!.lean

@@ -23,4 +23,4 @@ elab_rules : tactic
         let deps := (← collectForwardDeps #[mkFVar fvar] true).map (·.fvarId!)
         if ← deps.allM fun dep => return (← isClass? (lctx.get! dep).type).isNone then
           toClear := toClear ++ deps
-      tryClearMany goal toClear
+      goal.tryClearMany toClear

Mathlib/Tactic/ClearExcept.lean

@@ -21,4 +21,4 @@ elab_rules : tactic
         unless fvarIds.contains decl.fvarId do
           if let none ← isClass? decl.type then
             toClear := toClear.push decl.fvarId
-      tryClearMany goal toClear
+      goal.tryClearMany toClear

Mathlib/Tactic/Clear_.lean

@@ -13,4 +13,4 @@ elab (name := clear_) "clear_" : tactic =>
         if !str.isEmpty && str.front == '_' then
           if let none ← isClass? decl.type then
             toClear := toClear.push decl.fvarId
-    tryClearMany goal toClear
+    goal.tryClearMany toClear

Mathlib/Tactic/Constructor.lean

@@ -15,6 +15,6 @@ except that it does not reorder goals.
 -/
 elab "fconstructor " : tactic => withMainContext do
   let mvarIds' ←
-    Meta.constructor (cfg := {newGoals := .all}) (← getMainGoal)
+    (← getMainGoal).constructor (cfg := {newGoals := .all})
   Term.synthesizeSyntheticMVarsNoPostponing
   replaceMainGoal mvarIds'

Mathlib/Tactic/Ext.lean

@@ -61,7 +61,7 @@ scoped elab "ext_iff_type%" struct:ident : term => do
 
 elab "subst_eqs" : tactic =>
   open Elab.Tactic in
-  liftMetaTactic1 fun mvarId => substEqs mvarId
+  liftMetaTactic1 fun mvarId => mvarId.substEqs
 
 scoped macro "ext_proof%" : term =>
   `(fun {..} {..} => by intros; subst_eqs; rfl)
@@ -146,7 +146,7 @@ elab "apply_ext_lemma" : tactic => do
   let s ← saveState
   for lem in ← (extLemmas (← getEnv)).getMatch ty do
     try
-      liftMetaTactic (apply · (← mkConstWithFreshMVarLevels lem))
+      liftMetaTactic (·.apply (← mkConstWithFreshMVarLevels lem))
       return
     catch _ => s.restore
   throwError "no applicable extensionality lemma found for{indentExpr ty}"

Mathlib/Tactic/Have.lean

@@ -36,8 +36,8 @@ syntax "suffices" Parser.Term.haveIdLhs' : tactic
 open Elab Term in
 def haveLetCore (mvarId : MVarId) (name : Option Syntax) (bis : Array Syntax)
   (t : Option Syntax) (keepTerm : Bool) : TermElabM (MVarId × MVarId) :=
-  let declFn := if keepTerm then define else assert
-  withMVarContext mvarId do
+  let declFn := if keepTerm then MVarId.define else MVarId.assert
+  mvarId.withContext do
     let n := if let some n := name then n.getId else `this
     let elabBinders k := if bis.isEmpty then k #[] else elabBinders bis k
     let (mvar1, t, p) ← elabBinders fun es => do
@@ -46,9 +46,9 @@ def haveLetCore (mvarId : MVarId) (name : Option Syntax) (bis : Array Syntax)
       | some t => Tactic.elabTerm.go t none
       let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
       pure (p.mvarId!, ← mkForallFVars es t, ← mkLambdaFVars es p)
-    let (fvar, mvar2) ← intro1P (← declFn mvarId n t p)
+    let (fvar, mvar2) ← (← declFn mvarId n t p).intro1P
     if let some stx := name then
-      withMVarContext mvar2 do
+      mvar2.withContext do
         Term.addTermInfo' (isBinder := true) stx (mkFVar fvar)
     pure (mvar1, mvar2)