List.rotate vs List.rotateLeft

Stream: batteries

[Eric Wieser]

Presumably the former should be dropped from Std, as it exists with the longer name in core?

import Std
#eval List.rotate [1, 2, 3, 4] 1 = List.rotateLeft [1, 2, 3, 4] 1 -- true

(docs#List.rotateLeft, docs#List.rotate)

[Mario Carneiro]

There is also List.rotate' which is "the same as List.rotate but slower", by which I assume it means the same but with better (or at least different) defeqs

[Eric Wieser]

I assume that csimp should be used here then?