From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/success/guard.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'test-suite/success/guard.v') diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v index b9181d43..3a1c6dab 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. -- cgit v1.2.3