diff --git a/library/lang/Map.scala b/library/lang/Map.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8df83e6e1b678dfe2722515633f914ed93f3f76f
--- /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)
+}