# HG changeset patch
# User wenzelm
# Date 1533302951 -7200
# Node ID 8197c285726717113a30d14515ab52daad9ec549
# Parent  1d5ab386eaf05bc7da304f38c518b58007ae793a
more operations (as in ML);

diff -r 1d5ab386eaf0 -r 8197c2857267 src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Aug 03 15:04:24 2018 +0200
+++ b/src/Pure/library.scala	Fri Aug 03 15:29:11 2018 +0200
@@ -259,6 +259,15 @@
     result.toList
   }
 
+  def replicate[A](n: Int, a: A): List[A] =
+    if (n < 0) throw new IllegalArgumentException
+    else if (n == 0) Nil
+    else {
+      val res = new mutable.ListBuffer[A]
+      (1 to n).foreach(_ => res += a)
+      res.toList
+    }
+
 
   /* proper values */