We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 529c94b commit a4b6e82Copy full SHA for a4b6e82
MathlibTest/LibraryRewrite.lean
@@ -85,7 +85,7 @@ info: Pattern n + 1
85
· Std.PRange.succ n
86
Std.PRange.Nat.succ_eq
87
· (*...=n).size
88
- Std.PRange.Nat.size_Ric
+ Std.PRange.Nat.size_ric
89
· (↑n + 1).toNat
90
Int.toNat_natCast_add_one
91
0 commit comments