Merge pull request #527 from Seasawher/auto-update-branch

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `75f8adf6a6e95711bf49b848b590f2d123371a14`
+Mathlib version: `ef549b7b128a834178a5f25fbcdf75c3aa32deb7`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas
@@ -1490,11 +1490,6 @@ directly.
 ## to_additive
  Transport multiplicative to additive
 
-## to_additive_change_numeral
- Auxiliary attribute for `to_additive` that stores functions that have numerals as argument.
-Similar to `registerParametricAttribute` except that attributes do not
-have to be assigned in the same file as the declaration.
-
 ## to_additive_dont_translate
  Auxiliary attribute for `to_additive` stating that the operations on this type should not be translated.
 Similar to `registerParametricAttribute` except that attributes do not
@@ -1513,9 +1508,32 @@ have to be assigned in the same file as the declaration.
 ## to_app
 
 
+## to_dual
+ Transport to dual
+
+## to_dual_dont_translate
+ Auxiliary attribute for `to_dual` stating that the operations on this type should not be translated.
+Similar to `registerParametricAttribute` except that attributes do not
+have to be assigned in the same file as the declaration.
+
+## to_dual_ignore_args
+ Auxiliary attribute for `to_dual` stating that certain arguments are not dualized.
+Similar to `registerParametricAttribute` except that attributes do not
+have to be assigned in the same file as the declaration.
+
+## to_dual_relevant_arg
+ Auxiliary attribute for `to_dual` stating which arguments are the types with a dual structure.
+Similar to `registerParametricAttribute` except that attributes do not
+have to be assigned in the same file as the declaration.
+
 ## trans
  transitive relation
 
+## translate_change_numeral
+ Auxiliary attribute for `to_additive` that stores functions that have numerals as argument.
+Similar to `registerParametricAttribute` except that attributes do not
+have to be assigned in the same file as the declaration.
+
 ## try_tactic
  try_tactic elaborator
 

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `75f8adf6a6e95711bf49b848b590f2d123371a14`
+Mathlib version: `ef549b7b128a834178a5f25fbcdf75c3aa32deb7`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`
@@ -1887,6 +1887,13 @@ Some common uses:
     initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
   ```
 
+## insert_to_additive_translation
+Defined in: `Mathlib.Tactic.ToAdditive.commandInsert_to_additive_translation__`
+
+`insert_to_additive_translation mulName addName` inserts the translation `mulName ↦ addName`
+into the `to_additive` dictionary. This is useful for translating namespaces that don't (yet)
+have a corresponding translated declaration.
+
 ## irreducible_def
 Defined in: `Lean.Elab.Command.command_Irreducible_def____`
 

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `75f8adf6a6e95711bf49b848b590f2d123371a14`
+Mathlib version: `ef549b7b128a834178a5f25fbcdf75c3aa32deb7`
 
 ## Elab.async
 type: `Bool`
@@ -744,7 +744,7 @@ type: `Bool`
 
 default: `true`
 
-Linter, mostly used by `@[to_additive]`, that checks that the source declaration doesn't have certain attributes
+Linter, mostly used by translate attributes, that checks that the source declaration doesn't have certain attributes
 
 ## linter.flexible
 type: `Bool`
@@ -1194,34 +1194,34 @@ default: `false`
 
 
 
-## linter.toAdditiveExisting
+## linter.toAdditiveRelevantArg
 type: `Bool`
 
 default: `true`
 
-Linter used by `@[to_additive]` that checks whether the user correctly specified that
-    the additive declaration already exists
+Linter to check that the `relevant_arg` attribute is not given manually.
 
-## linter.toAdditiveGenerateName
+## linter.trailingWhitespace
 type: `Bool`
 
 default: `true`
 
-Linter used by `@[to_additive]` that checks if `@[to_additive]` automatically generates the user-given name
 
-## linter.toAdditiveRelevantArg
+
+## linter.translateExisting
 type: `Bool`
 
 default: `true`
 
-Linter to check that the `relevant_arg` attribute is not given manually.
+Linter used by translate attributes that checks whether the user correctly specified
+    that the translated declaration already exists
 
-## linter.trailingWhitespace
+## linter.translateGenerateName
 type: `Bool`
 
 default: `true`
 
-
+Linter used by translate attributes that checks if the given declaration name is equal to the automatically generated name
 
 ## linter.unnecessarySeqFocus
 type: `Bool`
@@ -5365,14 +5365,14 @@ default: `false`
 
 enable/disable tracing for the given module and submodules
 
-## trace.to_additive
+## trace.translate
 type: `Bool`
 
 default: `false`
 
 enable/disable tracing for the given module and submodules
 
-## trace.to_additive_detail
+## trace.translate_detail
 type: `Bool`
 
 default: `false`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `75f8adf6a6e95711bf49b848b590f2d123371a14`
+Mathlib version: `ef549b7b128a834178a5f25fbcdf75c3aa32deb7`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "75f8adf6a6e95711bf49b848b590f2d123371a14",
+   "rev": "ef549b7b128a834178a5f25fbcdf75c3aa32deb7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",