diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-09 14:25:41 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-09 14:25:41 +0000 |
commit | 01b8dc21e73e222dfe66488cf0a8a76fd0efdf10 (patch) | |
tree | 3c64f2609a5e6444243512fd918762fc1ea2293b /contrib/correctness/examples/extract.v | |
parent | f67fb6284009a7686ee51f4e6f44d9233de8b788 (diff) |
exemples Correctness
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1562 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/examples/extract.v')
-rw-r--r-- | contrib/correctness/examples/extract.v | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/contrib/correctness/examples/extract.v b/contrib/correctness/examples/extract.v new file mode 100644 index 000000000..e225ba187 --- /dev/null +++ b/contrib/correctness/examples/extract.v @@ -0,0 +1,43 @@ + +(* Tests d'extraction *) + +Require ProgramsExtraction. +Save State Ici "test extraction". + +(* exp *) + +Require exp. +Write Caml File "exp" [ i_exp r_exp ]. + +(* exp_int *) + +Restore State Ici. +Require exp_int. +Write Caml File "exp_int" [ i_exp r_exp ]. + +(* fact *) + +Restore State Ici. +Require fact. +Initialize x with (S (S (S O))). +Initialize y with O. +Write Caml File "fact" [ factorielle ]. + +(* fact_int *) + +Restore State Ici. +Require fact_int. +Initialize x with `3`. +Initialize y with `0`. +Write Caml File "fact_int" [ factorielle ]. + +(* Handbook *) + +Restore State Ici. +Require Handbook. +Initialize X with `3`. +Initialize Y with `3`. +Initialize Z with `3`. +Initialize N with `3`. +Initialize S with `3`. +Write Caml File "Handbook" [ pgm178 pgm186 pgm196 ]. |