chore(*): fix last line length and notation style linter errors (#10642)

These are the last non-module doc style linter errors (from https://github.com/leanprover-community/mathlib/blob/master/scripts/style-exceptions.txt). Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
leanprover-community · Dec 7, 2021 · 9031989 · 9031989
1 parent cd857f7
commit 9031989
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 6 deletions.
diff --git a/src/data/pfunctor/multivariate/M.lean b/src/data/pfunctor/multivariate/M.lean
@@ -40,7 +40,8 @@ that `A` is a possibly infinite tree.
 
 ## Reference
 
- * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
+ * Jeremy Avigad, Mario M. Carneiro and Simon Hudon.
+   [*Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
 -/
 
 universe u

diff --git a/src/data/pfunctor/multivariate/W.lean b/src/data/pfunctor/multivariate/W.lean
@@ -39,7 +39,8 @@ its valid paths to values of `α`
 
 ## Reference
 
- * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
+ * Jeremy Avigad, Mario M. Carneiro and Simon Hudon.
+   [*Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
 -/
 
 universes u v

diff --git a/src/data/qpf/multivariate/constructions/cofix.lean b/src/data/qpf/multivariate/constructions/cofix.lean
@@ -35,7 +35,8 @@ We define the relation `Mcongr` and take its quotient as the definition of `cofi
 
 ## Reference
 
- * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
+ * Jeremy Avigad, Mario M. Carneiro and Simon Hudon.
+   [*Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
 -/
 
 universe u

diff --git a/src/data/qpf/multivariate/constructions/fix.lean b/src/data/qpf/multivariate/constructions/fix.lean
@@ -44,7 +44,8 @@ See [avigad-carneiro-hudon2019] for more details.
 
 ## Reference
 
- * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
+ * Jeremy Avigad, Mario M. Carneiro and Simon Hudon.
+   [*Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
 -/
 
 universes u v

diff --git a/src/tactic/induction.lean b/src/tactic/induction.lean
@@ -1325,8 +1325,6 @@ meta def generalisation_mode_parser : lean.parser generalization_mode :=
   <|>
   pure (generalization_mode.generalize_all_except [])
 
-precedence `fixing`:0
-
 /--
 A variant of `tactic.interactive.induction`, with the following differences:
 

diff --git a/src/tactic/reserved_notation.lean b/src/tactic/reserved_notation.lean
@@ -47,6 +47,9 @@ reserve notation `to`
 -- used in `tactic/rcases.lean`
 precedence `?`:max
 
+-- used in `tactic/induction.lean`
+precedence `fixing`:0
+
 -- used in `order/lattice.lean`
 reserve infixl ` ⊓ `:70
 reserve infixl ` ⊔ `:65