diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite/success/Case15.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite/success/Case15.v')
-rw-r--r-- | test-suite/success/Case15.v | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v new file mode 100644 index 00000000..22944520 --- /dev/null +++ b/test-suite/success/Case15.v @@ -0,0 +1,48 @@ +(* Check compilation of multiple pattern-matching on terms non + apparently of inductive type *) + +(* Check that the non dependency in y is OK both in V7 and V8 *) +Check ([x;y:Prop;z]<[x][z]x=x \/ z=z>Cases x y z of + | O y z' => (or_introl ? (z'=z') (refl_equal ? O)) + | _ y O => (or_intror ?? (refl_equal ? O)) + | x y _ => (or_introl ?? (refl_equal ? x)) + end). + +(* Suggested by Pierre Letouzey (PR#207) *) +Inductive Boite : Set := + boite : (b:bool)(if b then nat else nat*nat)->Boite. + +Definition test := [B:Boite]<nat>Cases B of + (boite true n) => n +| (boite false (n,m)) => (plus n m) +end. + +(* Check lazyness of compilation ... future work +Inductive I : Set := c : (b:bool)(if b then bool else nat)->I. + +Check [x] + Cases x of + (c (true as y) (true as x)) => (if x then y else true) + | (c false O) => true | _ => false + end. + +Check [x] + Cases x of + (c true true) => true + | (c false O) => true + | _ => false + end. + +(* Devrait produire ceci mais trouver le type intermediaire est coton ! *) +Check + [x:I] + Cases x of + (c b y) => + (<[b:bool](if b then bool else nat)->bool>if b + then [y](if y then true else false) + else [y]Cases y of + O => true + | (S _) => false + end y) + end. +*) |