Mercurial > urweb
comparison src/elab_util.sml @ 2201:1091227f535a
Unnest properly in presence of kind polymorphism
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 20 Dec 2015 13:41:35 -0500 |
parents | 22117edf8fd3 |
children |
comparison
equal
deleted
inserted
replaced
2200:fc1c89627178 | 2201:1091227f535a |
---|---|
113 S.Return () | 113 S.Return () |
114 else | 114 else |
115 S.Continue (k, ())) k () of | 115 S.Continue (k, ())) k () of |
116 S.Return _ => true | 116 S.Return _ => true |
117 | S.Continue _ => false | 117 | S.Continue _ => false |
118 | |
119 fun foldB {kind, bind} ctx st k = | |
120 case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)), | |
121 bind = bind} ctx k st of | |
122 S.Continue (_, st) => st | |
123 | S.Return _ => raise Fail "ElabUtil.Kind.foldB: Impossible" | |
118 | 124 |
119 end | 125 end |
120 | 126 |
121 val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con) | 127 val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con) |
122 | 128 |