diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-07-01 12:25:12 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-01 12:25:12 -0400 |
| commit | f7d2bdce780d0333431829a8a788bdb208c0dcbc (patch) | |
| tree | 5316084519f313741563c016ac6733d03f892475 /src/lacweb.grm | |
| parent | 7628e1d8f7f8199531c9bc08a774c9a9e2bc5d63 (diff) | |
Disjointness assumptions in expressions
Diffstat (limited to 'src/lacweb.grm')
| -rw-r--r-- | src/lacweb.grm | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/lacweb.grm b/src/lacweb.grm index 39d30349..4bf03388 100644 --- a/src/lacweb.grm +++ b/src/lacweb.grm @@ -196,6 +196,7 @@ cexp : capps (capps) | FN SYMBOL DARROW cexp (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright)) | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright)) | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright)) + | cterm TWIDDLE cterm ARROW cexp (TDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) @@ -245,6 +246,7 @@ eexp : eapps (eapps) | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright)) | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright)) | FN SYMBOL DARROW eexp (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright)) + | FN cterm TWIDDLE cterm DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (cterm1left, eexpright)) | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright)) | eterm DOT ident (EField (eterm, ident), s (etermleft, identright)) |