Skip to content

Commit 3164384

Browse files
committed
version update
Fixes #1275
1 parent 19c9866 commit 3164384

File tree

2 files changed

+10
-6
lines changed

2 files changed

+10
-6
lines changed

LeanByExample/Tactic/Ring.lean

+5-1
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,11 @@ elab "#expand " t:macro_stx : command => do
7474
/--
7575
info: first
7676
| ring1
77-
| try_this ring_nf
77+
|
78+
try_this ring_nf"\n\nThe `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
79+
\nNote that `ring` works primarily in *commutative* rings. \
80+
If you have a noncommutative ring, abelian group or module, consider using \
81+
`noncomm_ring`, `abel` or `module` instead."
7882
-/
7983
#guard_msgs (info, drop warning) in
8084
#expand ring

lake-manifest.json

+5-5
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "653f17d0c439d2d9d55797995521660adc6df994",
8+
"rev": "ec10d9ba44225d66e790787d0f5b19a14830337e",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "master",
@@ -15,7 +15,7 @@
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "",
18-
"rev": "ebaada203996d763d17fbdda6a1da6c9cb55f1ad",
18+
"rev": "457c270d926709f41480d1880e27d95915fa7378",
1919
"name": "mdgen",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -35,7 +35,7 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "leanprover-community",
38-
"rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
38+
"rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
3939
"name": "LeanSearchClient",
4040
"manifestFile": "lake-manifest.json",
4141
"inputRev": "main",
@@ -65,7 +65,7 @@
6565
"type": "git",
6666
"subDir": null,
6767
"scope": "leanprover-community",
68-
"rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
68+
"rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
6969
"name": "aesop",
7070
"manifestFile": "lake-manifest.json",
7171
"inputRev": "master",
@@ -85,7 +85,7 @@
8585
"type": "git",
8686
"subDir": null,
8787
"scope": "leanprover-community",
88-
"rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625",
88+
"rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
8989
"name": "batteries",
9090
"manifestFile": "lake-manifest.json",
9191
"inputRev": "main",

0 commit comments

Comments
 (0)