summaryrefslogtreecommitdiff
path: root/src/elab_util.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml15
1 files changed, 15 insertions, 0 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 3c1860c7..b0bca7bf 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -68,6 +68,11 @@ fun mapfold f =
| KUnit => S.return2 kAll
+ | KTuple ks =>
+ S.map2 (ListUtil.mapfold mfk ks,
+ fn ks' =>
+ (KTuple ks', loc))
+
| KError => S.return2 kAll
| KUnif (_, _, ref (SOME k)) => mfk' k
@@ -180,6 +185,16 @@ fun mapfoldB {kind = fk, con = fc, bind} =
| CUnit => S.return2 cAll
+ | CTuple cs =>
+ S.map2 (ListUtil.mapfold (mfc ctx) cs,
+ fn cs' =>
+ (CTuple cs', loc))
+
+ | CProj (c, n) =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (CProj (c', n), loc))
+
| CError => S.return2 cAll
| CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
| CUnif _ => S.return2 cAll