From 93088f64354949767b555161d5291558dd07774f Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 27 Apr 2015 10:40:45 +0200
Subject: [PATCH] Sets, Maps in library

---
 doc/library.rst | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/doc/library.rst b/doc/library.rst
index 637d7e7f9..0f76bce89 100644
--- a/doc/library.rst
+++ b/doc/library.rst
@@ -268,3 +268,32 @@ in the object ``ListSpecs``:
 +---------------------------------------------------------------+--------------------------------------------------------+
 | ``scanVsFoldRight[A,B](l: List[A], z: B, f: (A,B) => B)``     | ``l.scanRight(f)(z).head == l.foldRight(f)(z)``        |
 +---------------------------------------------------------------+--------------------------------------------------------+
+
+Set[T], Map[T]
+--------------
+
+Leon uses its own Sets and Maps, which are defined in the ``leon.lang`` package.
+However, these classes are are not implemented within Leon.
+Instead, they are parsed into specialized trees.
+Methods of these classes are mapped to specialized trees within SMT solvers.
+For code generation, we rely on Java Sets and Maps.
+
+The API of these classes is a subset of the Scala API and can be found
+in the :ref:`purescala` section.
+
+Additionally, the following functions for Sets are provided in the
+``leon.collection`` package:
+
+
++-----------------------------------------------------------+-------------------------------------------+
+| Function signature                                        | Short description                         |
++===========================================================+===========================================+
+| ``setToList[A](set: Set[A]): List[A]``                    | Transforms the Set ``set`` into a List.   |
++-----------------------------------------------------------+-------------------------------------------+
+| ``setForall[A](set: Set[A], p: A => Boolean): Boolean``   | Tests whether predicate ``p`` holds       |
+|                                                           | for all elements of Set ``set``.          |
++-----------------------------------------------------------+-------------------------------------------+
+| ``setExists[A](set: Set[A], p: A => Boolean): Boolean``   | Tests whether predicate ``p`` holds       |
+|                                                           | for all elements of Set ``set``.          |
++-----------------------------------------------------------+-------------------------------------------+
+
-- 
GitLab