diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success/Case17.v | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success/Case17.v')
| -rw-r--r-- | test-suite/success/Case17.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v index 061e136e..66af9e0d 100644 --- a/test-suite/success/Case17.v +++ b/test-suite/success/Case17.v @@ -11,7 +11,7 @@ Variables (l0 : list bool) (rec : forall l' : list bool, length l' <= S (length l0) -> - {l'' : list bool & + {l'' : list bool & {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}). @@ -25,17 +25,17 @@ Check | inleft (existS _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end - :{l'' : list bool & + :{l'' : list bool & {t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}). - + (* The same but with relative links to l0 and rec *) - + Check (fun (l0 : list bool) (rec : forall l' : list bool, length l' <= S (length l0) -> - {l'' : list bool & + {l'' : list bool & {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) => match rec l0 (HHH _) with @@ -45,6 +45,6 @@ Check | inleft (existS _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end - :{l'' : list bool & + :{l'' : list bool & {t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}). |