diff --git a/library/collection/List.scala b/library/collection/List.scala index 11eccd24f6a4f14c1ee8b88ffe4a1ecb2cddeff0..60a5f25ec44aa9487cf96fa74af69b3b514d9e35 100644 --- a/library/collection/List.scala +++ b/library/collection/List.scala @@ -451,7 +451,13 @@ sealed abstract class List[T] { @ignore object List { - def apply[T](elems: T*): List[T] = ??? + def apply[T](elems: T*): List[T] = { + var l: List[T] = Nil[T]() + for (e <- elems) { + l = Cons(e, l) + } + l.reverse + } } @library diff --git a/library/math/package.scala b/library/math/package.scala index 04ec9e47583574122b7980e868487b4688f70e88..8eb5f347963f4599faeca8e1c58adda74b259aef 100644 --- a/library/math/package.scala +++ b/library/math/package.scala @@ -1,10 +1,18 @@ package leon +import leon.annotation._ package object math { + @library def min(i1: Int, i2: Int) = if (i1 <= i2) i1 else i2 + + @library def max(i1: Int, i2: Int) = if (i1 >= i2) i1 else i2 + + @library def min(i1: BigInt, i2: BigInt) = if (i1 <= i2) i1 else i2 + + @library def max(i1: BigInt, i2: BigInt) = if (i1 >= i2) i1 else i2 }