chore: lean bump 2022-10-20

Std/Classes/Dvd.lean

@@ -9,4 +9,4 @@ class Dvd (α : Type _) where
   /-- Divisibility. `a ∣ b` (typed as `\|`) means that there is some `c` such that `b = a * c`. -/
   dvd : α → α → Prop
 
-@[inheritDoc] infix:50 " ∣ " => Dvd.dvd
+@[inherit_doc] infix:50 " ∣ " => Dvd.dvd

Std/Classes/SetNotation.lean

@@ -96,13 +96,13 @@ macro_rules
   | `({$x:term, $xs:term,*}) => `(insert $x {$xs:term,*})
 
 /-- Unexpander for the `{ x }` notation. -/
-@[appUnexpander singleton]
+@[app_unexpander singleton]
 def singletonUnexpander : Lean.PrettyPrinter.Unexpander
   | `($_ $a) => `({ $a:term })
   | _ => throw ()
 
 /-- Unexpander for the `{ x, y, ... }` notation. -/
-@[appUnexpander insert]
+@[app_unexpander insert]
 def insertUnexpander : Lean.PrettyPrinter.Unexpander
   | `($_ $a { $ts,* }) => `({$a:term, $ts,*})
   | _ => throw ()

Std/Data/List/Basic.lean

@@ -436,7 +436,7 @@ inductive Sublist {α} : List α → List α → Prop
   /-- If `l₁` is a subsequence of `l₂`, then `a :: l₁` is a subsequence of `a :: l₂`. -/
   | cons₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)
 
-@[inheritDoc] scoped infixl:50 " <+ " => Sublist
+@[inherit_doc] scoped infixl:50 " <+ " => Sublist
 
 /--
 Split a list at an index.
@@ -742,11 +742,11 @@ substring of `l₂`, that is, `l₂` has the form `s ++ l₁ ++ t` for some `s,
 -/
 def isInfix (l₁ : List α) (l₂ : List α) : Prop := ∃ s t, s ++ l₁ ++ t = l₂
 
-@[inheritDoc] infixl:50 " <+: " => isPrefix
+@[inherit_doc] infixl:50 " <+: " => isPrefix
 
-@[inheritDoc] infixl:50 " <:+ " => isSuffix
+@[inherit_doc] infixl:50 " <:+ " => isSuffix
 
-@[inheritDoc] infixl:50 " <:+: " => isInfix
+@[inherit_doc] infixl:50 " <:+: " => isInfix
 
 /--
 `inits l` is the list of initial segments of `l`.

Std/Data/Nat/Gcd.lean

@@ -17,7 +17,7 @@ theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
   | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
   | _ + 1 => by simp [gcd_succ]
 
-@[elabAsElim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
+@[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
     (H0 : ∀n, P 0 n) (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) : P m n :=
   Nat.strongInductionOn (motive := fun m => ∀ n, P m n) m
     (fun

Std/Data/RBMap/Basic.lean

@@ -832,9 +832,9 @@ can be used in `for` loops or converted to an array or list.
 -/
 @[inline] def keys (t : RBMap α β cmp) : Keys α β cmp := t
 
-@[inline, inheritDoc keysArray] def Keys.toArray := @keysArray
+@[inline, inherit_doc keysArray] def Keys.toArray := @keysArray
 
-@[inline, inheritDoc keysList] def Keys.toList := @keysList
+@[inline, inherit_doc keysList] def Keys.toList := @keysList
 
 instance : Coe (Keys α β cmp) (Array α) := ⟨keysArray⟩
 
@@ -881,9 +881,9 @@ can be used in `for` loops or converted to an array or list.
 -/
 @[inline] def values (t : RBMap α β cmp) : Values α β cmp := t
 
-@[inline, inheritDoc valuesArray] def Values.toArray := @valuesArray
+@[inline, inherit_doc valuesArray] def Values.toArray := @valuesArray
 
-@[inline, inheritDoc valuesList] def Values.toList := @valuesList
+@[inline, inherit_doc valuesList] def Values.toList := @valuesList
 
 instance : Coe (Values α β cmp) (Array β) := ⟨valuesArray⟩
 
@@ -967,7 +967,7 @@ private unsafe def modifyImpl (t : RBMap α β cmp) (k : α) (f : β → β) : R
 This takes the element out of the tree while `f` runs,
 so it uses the element linearly if `t` is unshared.
 -/
-@[implementedBy modifyImpl] opaque modify (t : RBMap α β cmp) (k : α) (f : β → β) : RBMap α β cmp
+@[implemented_by modifyImpl] opaque modify (t : RBMap α β cmp) (k : α) (f : β → β) : RBMap α β cmp
 
 -- def modify (t : RBMap α β cmp) (k : α) (f : β → β) : RBMap α β cmp :=
 --   t.modifyP (cmp k ·.1) (fun (a, b) => (a, f b))
@@ -1000,7 +1000,7 @@ The element is used linearly if `t` is unshared.
 The `AlterWF` assumption is required because `f` may change
 the ordering properties of the element, which would break the invariants.
 -/
-@[implementedBy alterImpl]
+@[implemented_by alterImpl]
 opaque alter (t : RBMap α β cmp) (k : α) (f : Option β → Option β) : RBMap α β cmp
 
 -- @[specialize] def alter
@@ -1074,6 +1074,6 @@ end RBMap
 end Std
 open Std
 
-@[inheritDoc RBMap.ofList]
+@[inherit_doc RBMap.ofList]
 abbrev List.toRBMap (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
   RBMap.ofList l cmp

Std/Lean/NameMapAttribute.lean

@@ -26,7 +26,8 @@ def NameMapExtension.add [Monad M] [MonadEnv M] [MonadError M]
      ext.addEntry (← getEnv) (k, v) |> setEnv
 
 /-- Registers a new extension with the given name and type. -/
-def registerNameMapExtension (α) (name : Name) : IO (NameMapExtension α) := do
+def registerNameMapExtension (α) (name : Name := by exact decl_name%) :
+    IO (NameMapExtension α) := do
   registerSimplePersistentEnvExtension {
     name
     addImportedFn := fun ass => ass.foldl (init := ∅) fun
@@ -40,6 +41,8 @@ def registerNameMapExtension (α) (name : Name) : IO (NameMapExtension α) := do
 structure NameMapAttributeImpl (α : Type) where
   /-- The name of the attribute -/
   name : Name
+  /-- The declaration which creates the attribute -/
+  ref : Name := by exact decl_name%
   /-- The description of the attribute -/
   descr : String
   /-- This function is called when the attribute is applied.
@@ -50,7 +53,7 @@ structure NameMapAttributeImpl (α : Type) where
 /-- Similar to `registerParametricAttribute` except that attributes do not
 have to be assigned in the same file as the declaration. -/
 def registerNameMapAttribute (impl : NameMapAttributeImpl α) : IO (NameMapExtension α) := do
-  let ext ← registerNameMapExtension α impl.name
+  let ext ← registerNameMapExtension α impl.ref
   registerBuiltinAttribute {
     name := impl.name
     descr := impl.descr

Std/Tactic/Basic.lean

@@ -13,16 +13,16 @@ import Std.Lean.Tactic
 open Lean Parser.Tactic Elab Command Elab.Tactic Meta
 
 /-- `exfalso` converts a goal `⊢ tgt` into `⊢ False` by applying `False.elim`. -/
-macro "exfalso" : tactic => `(apply False.elim)
+macro "exfalso" : tactic => `(tactic| apply False.elim)
 
 /--
 `_` in tactic position acts like the `done` tactic: it fails and gives the list
 of goals if there are any. It is useful as a placeholder after starting a tactic block
 such as `by _` to make it syntactically correct and show the current goal.
 -/
-macro "_" : tactic => `({})
+macro "_" : tactic => `(tactic| {})
 
-@[inheritDoc failIfSuccess]
+@[inherit_doc failIfSuccess]
 syntax (name := failIfSuccessConv) "fail_if_success " Conv.convSeq : conv
 
 attribute [tactic failIfSuccessConv] evalFailIfSuccess
@@ -36,7 +36,7 @@ macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 
 /-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/
 macro "rwa " rws:rwRuleSeq loc:(location)? : tactic =>
-  `(tactic| rw $rws:rwRuleSeq $[$loc:location]?; assumption)
+  `(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption))
 
 /--
 Like `exact`, but takes a list of terms and checks that all goals are discharged after the tactic.

Std/Tactic/CoeExt.lean

@@ -42,7 +42,6 @@ instance : ToExpr CoeFnInfo where
 /-- The environment extension for tracking coercion functions for delaboration -/
 initialize coeExt : SimpleScopedEnvExtension (Name × CoeFnInfo) (NameMap CoeFnInfo) ←
   registerSimpleScopedEnvExtension {
-    name := `coe
     addEntry := fun st (n, i) => st.insert n i
     initial := {}
   }

Std/Tactic/Ext.lean

@@ -111,7 +111,7 @@ macro_rules
 `ext1 pat*` is like `ext pat*` except it only applies one extensionality lemma instead
 of recursing as much as possible.
 -/
-macro "ext1" xs:(colGt ppSpace rintroPat)* : tactic => `(tactic| apply_ext_lemma; rintro $xs*)
+macro "ext1" xs:(colGt ppSpace rintroPat)* : tactic => `(tactic| (apply_ext_lemma; rintro $xs*))
 
 -- TODO
 /-- `ext1? pat*` is like `ext1 pat*` but gives a suggestion on what pattern to use -/

Std/Tactic/Ext/Attr.lean

@@ -17,7 +17,6 @@ syntax "declare_ext_theorems_for" ident : command
 /-- The environment extension to track `@[ext]` lemmas. -/
 initialize extExtension : SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
   registerSimpleScopedEnvExtension {
-    name := `ext
     addEntry := fun dt (n, ks) => dt.insertCore ks n
     initial := {}
   }

Std/Tactic/GuardExpr.lean

@@ -77,9 +77,9 @@ Check equality of two expressions.
 * `guard_expr e = e'` checks that `e` and `e'` are definitionally equal.
 -/
 syntax (name := guardExpr) "guard_expr " term:51 equal term : tactic
-@[inheritDoc guardExpr] syntax (name := guardExprConv) "guard_expr " term:51 equal term : conv
+@[inherit_doc guardExpr] syntax (name := guardExprConv) "guard_expr " term:51 equal term : conv
 
-@[inheritDoc guardExpr, tactic guardExpr, tactic guardExprConv]
+@[inherit_doc guardExpr, tactic guardExpr, tactic guardExprConv]
 def evalGuardExpr : Tactic := fun
   | `(tactic| guard_expr $r $eq:equal $p)
   | `(conv| guard_expr $r $eq:equal $p) => withMainContext do
@@ -96,9 +96,9 @@ Check the target agrees with a given expression.
 * `guard_target = e` checks that the target is definitionally equal to `e`.
 -/
 syntax (name := guardTarget) "guard_target " equal term : tactic
-@[inheritDoc guardTarget] syntax (name := guardTargetConv) "guard_target " equal term : conv
+@[inherit_doc guardTarget] syntax (name := guardTargetConv) "guard_target " equal term : conv
 
-@[inheritDoc guardTarget, tactic guardTarget, tactic guardTargetConv]
+@[inherit_doc guardTarget, tactic guardTarget, tactic guardTargetConv]
 def evalGuardTarget : Tactic :=
   let go eq r getTgt := withMainContext do
     let r ← elabTerm r none
@@ -120,10 +120,10 @@ Check that a named hypothesis has a given type and/or value.
 -/
 syntax (name := guardHyp)
   "guard_hyp " term:max (colon term)? (colonEq term)? : tactic
-@[inheritDoc guardHyp] syntax (name := guardHypConv)
+@[inherit_doc guardHyp] syntax (name := guardHypConv)
   "guard_hyp " term:max (colon term)? (colonEq term)? : conv
 
-@[inheritDoc guardHyp, tactic guardHyp, tactic guardHypConv]
+@[inherit_doc guardHyp, tactic guardHyp, tactic guardHypConv]
 def evalGuardHyp : Tactic := fun
   | `(tactic| guard_hyp $h $[$c $ty]? $[$eq $val]?)
   | `(conv| guard_hyp $h $[$c $ty]? $[$eq $val]?) => withMainContext do

Std/Tactic/HaveI.lean

@@ -17,9 +17,9 @@ and subgoals, where the extra binding is inconvenient.
 namespace Std.Tactic
 
 /-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
-@[termParser] def «haveI» := leading_parser withPosition ("haveI " >> haveDecl) >> optSemicolon termParser
+@[term_parser] def «haveI» := leading_parser withPosition ("haveI " >> haveDecl) >> optSemicolon termParser
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
-@[termParser] def «letI» := leading_parser withPosition ("letI " >> haveDecl) >> optSemicolon termParser
+@[term_parser] def «letI» := leading_parser withPosition ("letI " >> haveDecl) >> optSemicolon termParser
 
 macro_rules
   | `(haveI $_ : $_ := $_; $_) => throwUnsupported -- handled by elab
@@ -48,6 +48,6 @@ elab_rules <= expectedType
       return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
 
 /-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
-macro "haveI " d:haveDecl : tactic => `(refine_lift haveI $d:haveDecl; ?_)
+macro "haveI " d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_)
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
-macro "letI " d:haveDecl : tactic => `(refine_lift letI $d:haveDecl; ?_)
+macro "letI " d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)

Std/Tactic/Lint/Basic.lean

@@ -96,10 +96,10 @@ and produces a list of linters. -/
 def getLinters (l : List Name) : CoreM (List NamedLinter) :=
   l.mapM getLinter
 
-/-- Defines the user attribute `stdLinter` for adding a linter to the default set. -/
+/-- Defines the `std_linter` attribute for adding a linter to the default set. -/
 initialize stdLinterAttr : TagAttribute ←
   registerTagAttribute
-    (name := `stdLinter)
+    (name := `std_linter)
     (descr := "Use this declaration as a linting test in #lint")
     (validate := fun name => do
       let constInfo ← getConstInfo name

Std/Tactic/Lint/Misc.lean

@@ -19,7 +19,7 @@ This file defines several small linters.
 -/
 
 /-- A linter for checking whether a declaration has a namespace twice consecutively in its name. -/
-@[stdLinter] def dupNamespace : Linter where
+@[std_linter] def dupNamespace : Linter where
   noErrorsFound := "No declarations have a duplicate namespace."
   errorsFound := "DUPLICATED NAMESPACES IN NAME:"
   test declName := do
@@ -32,7 +32,7 @@ This file defines several small linters.
 
 /-- A linter object for checking for unused arguments.
 We skip all declarations that contain `sorry` in their value. -/
-@[stdLinter] def unusedArguments : Linter where
+@[std_linter] def unusedArguments : Linter where
   noErrorsFound := "No unused arguments."
   errorsFound := "UNUSED ARGUMENTS."
   test declName := do
@@ -56,7 +56,7 @@ We skip all declarations that contain `sorry` in their value. -/
           return m!"argument {i+1} {arg} : {← inferType arg}") m!", "
 
 /-- A linter for checking definition doc strings -/
-@[stdLinter] def docBlame : Linter where
+@[std_linter] def docBlame : Linter where
   noErrorsFound := "No definitions are missing documentation."
   errorsFound := "DEFINITIONS ARE MISSING DOCUMENTATION STRINGS:"
   test declName := do
@@ -89,7 +89,7 @@ def docBlameThm : Linter where
 
 /-- A linter for checking whether the correct declaration constructor (definition or theorem)
 has been used. -/
-@[stdLinter] def defLemma : Linter where
+@[std_linter] def defLemma : Linter where
   noErrorsFound := "All declarations correctly marked as def/lemma."
   errorsFound := "INCORRECT DEF/LEMMA:"
   test declName := do
@@ -107,7 +107,7 @@ has been used. -/
     | _, _ => return none
 
 /-- A linter for missing checking whether statements of declarations are well-typed. -/
-@[stdLinter] def checkType : Linter where
+@[std_linter] def checkType : Linter where
   noErrorsFound :=
     "The statements of all declarations type-check with default reducibility settings."
   errorsFound := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS DO NOT TYPE-CHECK."
@@ -160,7 +160,7 @@ occur by themselves in a level. It is ok if *one* of `u` or `v` never occurs alo
 `(α : Type u) (β : Type (max u v))` is a occasionally useful method of saying that `β` lives in
 a higher universe level than `α`.
 -/
-@[stdLinter] def checkUnivs : Linter where
+@[std_linter] def checkUnivs : Linter where
   noErrorsFound :=
     "All declarations have good universe levels."
   errorsFound := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS. " ++
@@ -185,7 +185,7 @@ where `e₁` and `e₂` are identical exprs.
 We call declarations of this form syntactic tautologies.
 Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts
 with rfl when elaboration results in a different term than the user intended. -/
-@[stdLinter] def synTaut : Linter where
+@[std_linter] def synTaut : Linter where
   noErrorsFound :=
     "No declarations are syntactic tautologies."
   errorsFound := "THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES. " ++
@@ -225,7 +225,7 @@ def findUnusedHaves (e : Expr) : MetaM (Array MessageData) := do
 /-- A linter for checking that declarations don't have unused term mode have statements. We do not
 tag this as `@[stdLlinter]` so that it is not in the default linter set as it is slow and an
 uncommon problem. -/
-@[stdLinter] def unusedHavesSuffices : Linter where
+@[std_linter] def unusedHavesSuffices : Linter where
   noErrorsFound := "No declarations have unused term mode have statements."
   errorsFound := "THE FOLLOWING DECLARATIONS HAVE INEFFECTUAL TERM MODE HAVE/SUFFICES BLOCKS. " ++
     "In the case of `have` this is a term of the form `have h := foo, bar` where `bar` does not " ++

Std/Tactic/Lint/Simp.lean

@@ -102,7 +102,7 @@ def formatLemmas (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
   `(tactic| simp only [$[$args:ident],*])
 
 /-- A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire. -/
-@[stdLinter] def simpNF : Linter where
+@[std_linter] def simpNF : Linter where
   noErrorsFound := "All left-hand sides of simp lemmas are in simp-normal form."
   errorsFound := "SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
 see note [simp-normal form] for tips how to debug this.
@@ -193,7 +193,7 @@ Here are some tips depending on the error raised by the linter:
 A linter for simp lemmas whose lhs has a variable as head symbol,
 and which hence never fire.
 -/
-@[stdLinter] def simpVarHead : Linter where
+@[std_linter] def simpVarHead : Linter where
   noErrorsFound :=
     "No left-hand sides of a simp lemma has a variable as head symbol."
   errorsFound := "LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.
@@ -206,7 +206,7 @@ Some simp lemmas have a variable as head symbol of the left-hand side:"
     return m!"Left-hand side has variable as head symbol: {headSym}"
 
 /-- A linter for commutativity lemmas that are marked simp. -/
-@[stdLinter] def simpComm : Linter where
+@[std_linter] def simpComm : Linter where
   noErrorsFound := "No commutativity lemma is marked simp."
   errorsFound := "COMMUTATIVITY LEMMA IS SIMP.
 Some commutativity lemmas are simp lemmas:"

Std/Tactic/NoMatch.lean

@@ -17,7 +17,7 @@ Along the same lines, `fun.` is a nullary pattern matching function; it is equiv
 impossible pattern. The `match x with.` and `intro.` tactics do the same thing but in tactic mode.
 -/
 namespace Std.Tactic
-open Lean Elab Term
+open Lean Elab Term Parser.Term
 
 /--
 The syntax `match x with.` is a variant of `nomatch x` which supports pattern matching on multiple
@@ -27,7 +27,7 @@ syntax:lead (name := noMatch) "match " matchDiscr,* " with" "." : term
 
 open private elabMatchAux waitExpectedType from Lean.Elab.Match in
 /-- Elaborator for `match x with.` -/
-@[termElab noMatch] def elabNoMatch' : TermElab
+@[term_elab noMatch] def elabNoMatch' : TermElab
 | `(match $discrs,* with.), expectedType? => do
   let discrs := discrs.getElems
   for h : i in [0:discrs.size] do
@@ -53,9 +53,9 @@ elab (name := noFun) tk:"fun" "." : term <= expectedType => do
         return ((⟨← `(a)⟩ : Ident), ← `(matchDiscr| a))
   elabTerm (← `(@fun%$tk $binders:ident* => match%$tk $discrs:matchDiscr,* with.)) expectedType
 
-@[inheritDoc noFun] macro tk:"λ" "." : term => `(fun%$tk .)
+@[inherit_doc noFun] macro tk:"λ" "." : term => `(fun%$tk .)
 
-@[inheritDoc noMatch] macro "match " discrs:matchDiscr,* " with" "." : tactic =>
+@[inherit_doc noMatch] macro "match " discrs:matchDiscr,* " with" "." : tactic =>
   `(tactic| exact match $discrs,* with.)
 
 /--