From 8438cb2c237f44b0fe214c5472222d84eeb0f5a0 Mon Sep 17 00:00:00 2001 From: Viktor Kuncak <viktor.kuncak@epfl.ch> Date: Sun, 26 Apr 2015 15:46:07 -0700 Subject: [PATCH] doc: what to import. --- doc/gettingstarted.rst | 2 +- doc/library.rst | 31 ++++++++++++++++++++++++++++++- 2 files changed, 31 insertions(+), 2 deletions(-) diff --git a/doc/gettingstarted.rst b/doc/gettingstarted.rst index 2401d2573..09ddf3543 100644 --- a/doc/gettingstarted.rst +++ b/doc/gettingstarted.rst @@ -94,5 +94,5 @@ and get something like this For more details on how to build Leon from sources that can be used directly from the shell, see :ref:`installation`. In addition to invoking `./leon --help` you -may wish to consult :ref:`cmdlineoptions`. +may wish to consult :ref:`cmdlineoptions` options. diff --git a/doc/library.rst b/doc/library.rst index b49c3881b..3778e8e03 100644 --- a/doc/library.rst +++ b/doc/library.rst @@ -3,7 +3,36 @@ Leon Library ============ -Leon defines its own versions of most data structures. One of the reasons is to ensure that these operations can be correctly mapped to mathematical functions and relations inside of SMT solvers, largely defined by the SMT-LIB standard (see http://www.smt-lib.org/). +Leon defines its own versions of most data structures. One +of the reasons is to ensure that these operations can be +correctly mapped to mathematical functions and relations +inside of SMT solvers, largely defined by the SMT-LIB +standard (see http://www.smt-lib.org/). + +To use Leon's libraries, you need to use the appropriate +`import` directive at the top of Leon's compilation units. +Here is a quick summary of what to import. + ++--------------------------------+----------------------------------------------------+ +| Package to import | What it gives access to | ++================================+====================================================+ +|`leon.annotation` | Leon annotations, e.g. @induct | ++--------------------------------+----------------------------------------------------+ +|`leon.lang` | `Map`, `Set`, `holds`, `passes`, `invariant` | ++--------------------------------+----------------------------------------------------+ +|`leon.collection.List` | List[T] + ++--------------------------------+----------------------------------------------------+ +|`leon.collection.Option` | Option[T] + ++--------------------------------+----------------------------------------------------+ +|`leon.lang.string` | String + ++--------------------------------+----------------------------------------------------+ +|`leon.lang.xlang` | epsilon + ++--------------------------------+----------------------------------------------------+ +|`leon.lang.synthesis` | choose, ???, ?, ?! + ++--------------------------------+----------------------------------------------------+ + +In the sequel we outline some of the libraries. To learn more, we encourage you to +look in the `library/` subdirectory of Leon distribution. List ^^^^ -- GitLab