From 549ec0e305ec6dc7ad8f6e17b062ac9f210a5ae0 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 19 May 2015 11:24:25 +0200
Subject: [PATCH] List.apply should be Scala-executable. Fix leon.math not
being @library
---
library/collection/List.scala | 8 +++++++-
library/math/package.scala | 8 ++++++++
2 files changed, 15 insertions(+), 1 deletion(-)
diff --git a/library/collection/List.scala b/library/collection/List.scala
index 11eccd24f..60a5f25ec 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 04ec9e475..8eb5f3479 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
}
--
GitLab