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