diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-09-07 13:47:10 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-09-07 13:47:10 -0400 |
| commit | 725ce6746ebcd76fc3a8c7aa3248805493d71fa0 (patch) | |
| tree | 8292403aa4aeb15da4f89189e97210b353704140 /src/urweb.grm | |
| parent | 8443e6fb491fa8c8877e53e6548e2fca401e24d5 (diff) | |
Elaborated 'insert'
Diffstat (limited to 'src/urweb.grm')
| -rw-r--r-- | src/urweb.grm | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/urweb.grm b/src/urweb.grm index 6cb41890..6f355c43 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -607,6 +607,14 @@ eexp : eapps (eapps) in (EApp (e, (EAbs (SYMBOL, NONE, eexp2), loc)), loc) end) + | UNIT LARROW eexp SEMI eexp (let + val loc = s (UNITleft, eexp2right) + val e = (EVar (["Basis"], "bind"), loc) + val e = (EApp (e, eexp1), loc) + val t = (TRecord (CRecord [], loc), loc) + in + (EApp (e, (EAbs ("_", SOME t, eexp2), loc)), loc) + end) | eexp EQ eexp (native_op ("eq", eexp1, eexp2, s (eexp1left, eexp2right))) | eexp NE eexp (native_op ("ne", eexp1, eexp2, s (eexp1left, eexp2right))) |