From 725ce6746ebcd76fc3a8c7aa3248805493d71fa0 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 7 Sep 2008 13:47:10 -0400 Subject: Elaborated 'insert' --- src/urweb.grm | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/urweb.grm') 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))) -- cgit v1.2.3