diff options
author | 2004-07-28 21:54:47 +0000 | |
---|---|---|
committer | 2004-07-28 21:54:47 +0000 | |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/correctness/examples/extract.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
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 00000000..e225ba18 --- /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 ]. |