diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-06 12:57:04 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-06 12:57:04 -0500 |
commit | 26faf65015eb8d6a9ce57772feb05c7dc63a1dea (patch) | |
tree | 39ca4f0aefad1b7f21da8f3cd156ff79fed5a609 /src/Util | |
parent | 05c07764874c37b6d826e177bf8b90b5fb44349c (diff) |
Deduplicate some code
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/CPSUtil.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v index fc7d43b93..927d071f6 100644 --- a/src/Util/CPSUtil.v +++ b/src/Util/CPSUtil.v @@ -115,14 +115,12 @@ Definition id_tuple'_with_alt_cps {R A n} (value value_for_alt : forall R, (Tuple.tuple' A n -> R) -> R) (f : Tuple.tuple' A n -> R) : R - := dlet z := id_tuple'_with_alt (value _ id) (value_for_alt _ id) in - f z. + := id_tuple'_with_alt_cps' (value _) (value_for_alt _) f. Definition id_tuple_with_alt_cps {R A n} (value value_for_alt : forall R, (Tuple.tuple A n -> R) -> R) (f : Tuple.tuple A n -> R) : R - := dlet z := id_tuple_with_alt (value _ id) (value_for_alt _ id) in - f z. + := id_tuple_with_alt_cps' (value _) (value_for_alt _) f. Definition id_tuple'_with_alt_cps_correct {R A n} value value_for_alt f : @id_tuple'_with_alt_cps R A n value value_for_alt f = f (id_tuple'_with_alt (value _ id) (value_for_alt _ id)) |