diff --git a/docs/attributes.md b/docs/attributes.md index 44823a2..f9ea830 100644 --- a/docs/attributes.md +++ b/docs/attributes.md @@ -1,6 +1,6 @@ # Attributes -Mathlib version: `53815d4e7dfe51eef5f197cc28f93404bd97893d` +Mathlib version: `4203807415a6e558c850c2a7d406fc948359f50e` ## aesop Register a declaration as an Aesop rule. diff --git a/docs/commands.md b/docs/commands.md index cc3ba90..85de15c 100644 --- a/docs/commands.md +++ b/docs/commands.md @@ -1,6 +1,6 @@ # Commands -Mathlib version: `53815d4e7dfe51eef5f197cc28f93404bd97893d` +Mathlib version: `4203807415a6e558c850c2a7d406fc948359f50e` ## \#adaptation_note Defined in: `adaptationNoteCmd` diff --git a/docs/options.md b/docs/options.md index 4b9158c..62de5f9 100644 --- a/docs/options.md +++ b/docs/options.md @@ -1,6 +1,6 @@ # Options -Mathlib version: `53815d4e7dfe51eef5f197cc28f93404bd97893d` +Mathlib version: `4203807415a6e558c850c2a7d406fc948359f50e` ## Elab.async type: `Bool` diff --git a/docs/tactics.md b/docs/tactics.md index 417d60d..86fa167 100644 --- a/docs/tactics.md +++ b/docs/tactics.md @@ -1,6 +1,6 @@ # Tactics -Mathlib version: `53815d4e7dfe51eef5f197cc28f93404bd97893d` +Mathlib version: `4203807415a6e558c850c2a7d406fc948359f50e` ## \#adaptation_note Defined in: `«tactic#adaptation_note_»` @@ -3975,7 +3975,8 @@ h: a = 1 ⊢ a + 1 + 1 + a + a = 5 -/ ``` -Notice that the second occurrence of `a` from the left has been rewritten by `nth_rewrite`. +Notice that the second and third occurrences of `a` from the left have been rewritten by +`nth_rewrite`. To understand the importance of order of precedence, consider the example below ```lean @@ -4027,7 +4028,8 @@ h: a = 1 ⊢ a + 1 + 1 + a + a = 5 -/ ``` -Notice that the second occurrence of `a` from the left has been rewritten by `nth_rewrite`. +Notice that the second and third occurrences of `a` from the left have been rewritten by +`nth_rw`. To understand the importance of order of precedence, consider the example below ```lean diff --git a/lake-manifest.json b/lake-manifest.json index b9d9126..b6d2e37 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "53815d4e7dfe51eef5f197cc28f93404bd97893d", + "rev": "4203807415a6e558c850c2a7d406fc948359f50e", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master",