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 1e5d986 commit 9cb732cCopy full SHA for 9cb732c
tests/lean/run/versoDocs.lean
@@ -89,7 +89,7 @@ If {lean}`xs.size ≤ n`, then {lean}`rot n xs = rot (n % xs.size) xs`.
89
Read more about {manual section "Array"}[arrays] in the Lean language reference.
90
-/
91
def rot (n : Nat) (xs : Array α) : Array α :=
92
- xs[n...*].copy ++ xs[*...n].copy
+ xs[n...*] ++ xs[*...n]
93
94
#eval rot 2 #[1, 2, 3]
95
0 commit comments