From 9190ccf8833e179e67db5500911376abcf8ad581 Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Tue, 29 Oct 2019 16:06:48 -0700
Subject: [PATCH] Add replicate to base/Data.List.

---
 libs/base/Data/List.idr | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
index 6c63b6d..8a0e5d2 100644
--- a/libs/base/Data/List.idr
+++ b/libs/base/Data/List.idr
@@ -121,6 +121,13 @@ public export
 reverse : List a -> List a
 reverse = reverseOnto []
 
+||| Construct a list with `n` copies of `x`.
+||| @ n how many copies
+||| @ x the element to replicate
+public export
+replicate : (n : Nat) -> (x : a) -> List a
+replicate Z     _ = []
+replicate (S n) x = x :: replicate n x
 
 ||| Compute the intersect of two lists by user-supplied equality predicate.
 export