summaryrefslogtreecommitdiff
path: root/src/urweb.grm
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-12 12:21:54 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-12 12:21:54 -0400
commit19b9eee2a968e9fe577792a48d0b4cf931165874 (patch)
tree62139cb8c7c3aa9f402a76b19a206cef58cad0d1 /src/urweb.grm
parenteb45f499c2e18f154ad59d75cf29c3903af5c725 (diff)
Basis and Top syntax-highlight, indent, parse, and type-check
Diffstat (limited to 'src/urweb.grm')
-rw-r--r--src/urweb.grm14
1 files changed, 7 insertions, 7 deletions
diff --git a/src/urweb.grm b/src/urweb.grm
index 3c270100..1879b241 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -714,13 +714,6 @@ earg : SYMBOL kcolon kind (fn (e, t) =>
((EAbs ("_", SOME cexp, e), loc),
(TFun (cexp, t), loc))
end)
- | cterm TWIDDLE cterm (fn (e, t) =>
- let
- val loc = s (cterm1left, cterm2right)
- in
- ((EDisjoint (cterm1, cterm2, e), loc),
- (CDisjoint (cterm1, cterm2, t), loc))
- end)
| eargp (eargp)
eargp : SYMBOL (fn (e, t) =>
@@ -773,6 +766,13 @@ eargp : SYMBOL (fn (e, t) =>
((EDisjoint (cterm1, cterm2, e), loc),
(CDisjoint (cterm1, cterm2, t), loc))
end)
+ | LBRACK cterm TWIDDLE cterm RBRACK(fn (e, t) =>
+ let
+ val loc = s (LBRACKleft, RBRACKright)
+ in
+ ((EDisjoint (cterm1, cterm2, e), loc),
+ (CDisjoint (cterm1, cterm2, t), loc))
+ end)
eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
| LPAREN etuple RPAREN (let