diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-17 22:37:26 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-18 11:02:14 -0400 |
commit | a426187067726ecb0362aabe12c3877166e427a0 (patch) | |
tree | af46a607b5f63c5d6ecf034bef7d4d20a10007d2 /src/Util | |
parent | b5c975c9b5a7cf522d9bd94a7843b96d91f64a9b (diff) |
Allow instantiating type arguments without reducing matches
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/CPSUtil.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v index f8d51e5b3..9b249b460 100644 --- a/src/Util/CPSUtil.v +++ b/src/Util/CPSUtil.v @@ -325,12 +325,12 @@ Module Tuple. := fun ts R => @mapi_with'_cps_specialized R T A B (fun n t a => @f n t a R) n i start ts. Definition mapi_with_cps {S A B n} - (f: nat->S->A->forall {T}, (S*B->T)->T) (start:S) - : tuple A n -> forall {T}, (S * tuple B n->T)->T := - match n as n0 return (tuple A n0 -> forall {T}, (S * tuple B n0->T)->T) with - | O => fun ys {T} ret => ret (start, tt) - | S n' => fun ys {T} ret => mapi_with'_cps 0%nat f start ys ret - end. + (f: nat->S->A->forall {T}, (S*B->T)->T) (start:S) (ys:tuple A n) {T} + : (S * tuple B n->T)->T := + match n as n0 return (tuple A n0 -> (S * tuple B n0->T)->T) with + | O => fun ys ret => ret (start, tt) + | S n' => fun ys ret => mapi_with'_cps 0%nat f start ys ret + end ys. Lemma unfold_mapi_with'_cps {T A B n} i (f: nat->T->A->forall {R}, (T*B->R)->R) (start:T) |