Commit 83bd9430 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

yet another paragraph of documentation

parent 2cc3c176
...@@ -80,6 +80,18 @@ containing theory \texttt{Int}. Theories referred to without prefix ...@@ -80,6 +80,18 @@ containing theory \texttt{Int}. Theories referred to without prefix
either appear earlier in the current file, \eg\ \texttt{List}, or are either appear earlier in the current file, \eg\ \texttt{List}, or are
predefined. predefined.
The next declaration defines a recursive function, \emph{length},
which computes the length of a list. The \texttt{logic} keyword is
used to introduce or define both function and predicate symbols.
\why\ checks every recursive, or mutually recursive, definition for
termination. Basically, we require a lexicographic and structural
descent for every recursive call for some reordering of arguments.
Note that matching must be exhaustive and that every \texttt{match}
expression must be terminated by the \texttt{end} keyword.
The last declaration in theory \texttt{Length} is a lemma stating that
the length of a list is non-negative.
% \section{Terms and Formulas} *) % \section{Terms and Formulas} *)
% \section{Declarations, Theories} *) % \section{Declarations, Theories} *)
......
...@@ -4,11 +4,6 @@ theory List ...@@ -4,11 +4,6 @@ theory List
type list 'a = Nil | Cons 'a (list 'a) type list 'a = Nil | Cons 'a (list 'a)
use import bool.Bool
logic x : int = match 1,2 with X u,y -> 3 end
end end
theory Length theory Length
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment