Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit ac1f7b76 authored by MARCHE Claude's avatar MARCHE Claude

improved documentation of theory creation by API

parent bbdcd12d
......@@ -428,6 +428,27 @@ We can inspect what we did for example by printing that theory:
let () = printf "@[theory is:@\n%a@]@." Pretty.print_theory my_theory
which outputs
theory is:
theory My_theory
(* use BuiltIn *)
goal goal1 : true \/ false
predicate A
predicate B
goal goal2 : A /\ B -> A
(* use int.Int *)
goal goal3 : (2 + 2) = 4
goal goal4 : forall x:int. (x * x) >= 0
From a theory, one can compute at once all the proof tasks it contains
as follows:
......@@ -435,7 +456,8 @@ as follows:
let my_tasks : Task.task list =
List.rev (Task.split_theory my_theory None None)
reversing the list is don because the tasks are returned in reverse order.
Note that the tasks are returned in reverse order, so we reverse the
list above.
We can check our generated tasks by printing them:
......@@ -461,8 +483,8 @@ One can run provers on those tasks exactly as we did above.
\section{Proof sessions}
See example \verb|examples/| for an example on how
to manipulate proof sessions from an OCaml program.
See the example \url{examples/} of the distribution for
an illustration on how to manipulate proof sessions from an OCaml program.
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