diff options
author | 2001-05-10 15:09:46 +0000 | |
---|---|---|
committer | 2001-05-10 15:09:46 +0000 | |
commit | 9dcc0b08f9d62ab8fd0f20a2c80dc1d5a5d56a26 (patch) | |
tree | 70a3f12b44b995cb14877c15165eeb632147c01a | |
parent | fa04b2438319c763ac6d1fd07ecdfd47a0663b2c (diff) |
exemples Magic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1742 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/extraction/test_extraction.v | 47 |
1 files changed, 43 insertions, 4 deletions
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v index 92aba71a0..218bb7141 100644 --- a/contrib/extraction/test_extraction.v +++ b/contrib/extraction/test_extraction.v @@ -126,10 +126,49 @@ Extraction test0. Extraction eq. Extraction eq_rec. -(* mutual fixpoints on many sorts ? *) - - (* TODO *) - (* example with more arguments that given by the type *) Extraction (nat_rec [n:nat]nat->nat [n:nat]O [n:nat][f:nat->nat]f O O). + +(* propagation of type parameters *) + +Inductive tp1 : Set := + T : (C:Set)(c:C)tp2 -> tp1 with tp2 : Set := T' : tp1->tp2. + +Inductive tp1bis : Set := + Tbis : tp2bis -> tp1bis +with tp2bis : Set := T'bis : (C:Set)(c:C)tp1bis->tp2bis. + +(* example needing Obj.magic *) + +(* hybrids *) + +Definition PropSet := [b:bool]if b then Prop else Set. +Extraction PropSet. + +Definition natbool := [b:bool]if b then nat else bool. +Extraction natbool. + +Definition zerotrue := + [b:bool]<natbool> Cases b of true => O | false => true end. +Extraction zerotrue. + +Definition natProp := [b:bool]<[b:bool]Type>if b then nat else Prop. + +Definition zeroTrue := + [b:bool]<natProp> Cases b of true => O | false => True end. +Extraction zeroTrue. + +Definition natTrue := [b:bool]<[b:bool]Type>if b then nat else True. + +Definition zeroprop := + [b:bool]<natTrue> Cases b of true => O | false => I end. +Extraction zeroprop. + +(* instanciations Type -> Prop *) + +(* Prop applied to Prop *) + +(* polymorphic f applied several times *) + + |