From cdab1dac5dd82dda33f3dc8b83fb3cd936d13ebd Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <ekneuss@gmail.com> Date: Mon, 20 Apr 2015 16:09:00 +0200 Subject: [PATCH] Add map definition --- library/lang/Map.scala | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 library/lang/Map.scala diff --git a/library/lang/Map.scala b/library/lang/Map.scala new file mode 100644 index 000000000..8df83e6e1 --- /dev/null +++ b/library/lang/Map.scala @@ -0,0 +1,15 @@ +package leon.lang +import leon.annotation._ + +object Map { + def empty[A,B] = Map[A,B]() +} + +@ignore +case class Map[A, B](elems: (A, B)*) { + def apply(k: A): B = ??? + def ++(b: Map[A, B]): Map[A,B] = ??? + def updated(k: A, v: B): Map[A,B] = ??? + def contains(a: A): Boolean = ??? + def isDefinedAt(a: A): Boolean = contains(a) +} -- GitLab