diff src/elab_util.sml @ 493:ae03d09043c1

Add CutMulti
author Adam Chlipala <adamc@hcoop.net>
date Tue, 11 Nov 2008 19:20:37 -0500
parents d34834af4512
children 44958d74c43f
line wrap: on
line diff
--- a/src/elab_util.sml	Tue Nov 11 18:39:38 2008 -0500
+++ b/src/elab_util.sml	Tue Nov 11 19:20:37 2008 -0500
@@ -338,6 +338,15 @@
                                                   fn rest' =>
                                                      (ECut (e', c', {field = field', rest = rest'}), loc)))))
 
+              | ECutMulti (e, c, {rest}) =>
+                S.bind2 (mfe ctx e,
+                      fn e' =>
+                         S.bind2 (mfc ctx c,
+                              fn c' =>
+                                 S.map2 (mfc ctx rest,
+                                      fn rest' =>
+                                         (ECutMulti (e', c', {rest = rest'}), loc))))
+
               | EFold k =>
                 S.map2 (mfk k,
                          fn k' =>