diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-09-19 09:55:49 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-19 09:55:49 +0200 |
commit | dd4a532455258badbc057b3780bf99e556d8c07a (patch) | |
tree | 481c79f197770f2a44e5cd44455a40a5f9cdf37f /test-suite/success | |
parent | 296941dc97d53817cc58b4687ed99168e1dd33a9 (diff) | |
parent | d6aa9482b7f0e09e06b844c59950211ca3bf9270 (diff) |
Merge PR #920: kernel: bugfix in filter_stack_domain.
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/guard.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v index b9181d430..83d47dc68 100644 --- a/test-suite/success/guard.v +++ b/test-suite/success/guard.v @@ -9,3 +9,20 @@ Check let x (f:nat->nat) k := f k in | 0 => 0 | S k => f F k (* here Rel 3 = F ! *) end. + +(** Commutation of guard condition allows recursive calls on functional arguments, + despite rewriting in their domain types. *) +Inductive foo : Type -> Type := +| End A : foo A +| Next A : (A -> foo A) -> foo A. + +Definition nat : Type := nat. + +Fixpoint bar (A : Type) (e : nat = A) (f : foo A) {struct f} : nat := +match f with +| End _ => fun _ => O +| Next A g => fun e => + match e in (_ = B) return (B -> foo A) -> nat with + | eq_refl => fun (g' : nat -> foo A) => bar A e (g' O) + end g +end e.
\ No newline at end of file |