Mercurial > urweb
comparison src/elab_util.sml @ 42:b3fbbc6cb1e5
Elaborating 'where'
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 19 Jun 2008 16:35:40 -0400 |
parents | 1405d8c26790 |
children | abb2b32c19fb |
comparison
equal
deleted
inserted
replaced
41:1405d8c26790 | 42:b3fbbc6cb1e5 |
---|---|
368 S.bind2 (sg ctx s1, | 368 S.bind2 (sg ctx s1, |
369 fn s1' => | 369 fn s1' => |
370 S.map2 (sg (bind (ctx, Str (m, s1'))) s2, | 370 S.map2 (sg (bind (ctx, Str (m, s1'))) s2, |
371 fn s2' => | 371 fn s2' => |
372 (SgnFun (m, n, s1', s2'), loc))) | 372 (SgnFun (m, n, s1', s2'), loc))) |
373 | SgnWhere (sgn, x, c) => | |
374 S.bind2 (sg ctx sgn, | |
375 fn sgn' => | |
376 S.map2 (con ctx c, | |
377 fn c' => | |
378 (SgnWhere (sgn', x, c'), loc))) | |
373 | SgnError => S.return2 sAll | 379 | SgnError => S.return2 sAll |
374 in | 380 in |
375 sg | 381 sg |
376 end | 382 end |
377 | 383 |