Def Vector.«repeat»

Modification history

2023-01-16 07:17

Mathlib/Data/Vector.lean

Refactor: drop `List.repeat` (#1579) …

Deleted Vector.«repeat»View on Github →

2022-12-12 18:44

Mathlib/Data/Vector.lean

feat: port Data.Vector from lean-core (#834) …

Added Vector.«repeat»View on Github →