We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 03ee6e8 commit 81dcfb9Copy full SHA for 81dcfb9
1 file changed
MathlibTest/LibraryRewrite.lean
@@ -82,10 +82,14 @@ Pattern ∀ (p : P), Q p
82
info: Pattern n + 1
83
· n.succ
84
Nat.add_one
85
+· (*...=n).size
86
+ Nat.size_ric
87
+· (*...=n).toArray.size
88
+ Nat.size_toArray_ric
89
+· (*...=n).toList.length
90
+ Nat.length_toList_ric
91
· Std.PRange.succ n
92
Std.PRange.Nat.succ_eq
-· (*...=n).size
- Std.PRange.Nat.size_ric
93
· (↑n + 1).toNat
94
Int.toNat_natCast_add_one
95
@@ -106,6 +110,8 @@ Pattern n + m
106
110
Nat.add_right_max_self
107
111
· max n (n + 1)
108
112
Nat.max_add_right_self
113
+· Std.PRange.succMany 1 n
114
+ Std.PRange.Nat.succMany_eq
109
115
116
Pattern a + b
117
· 1 + n
0 commit comments