Mercurial > urweb
diff src/lacweb.grm @ 85:1f85890c9846
Disjointness assumptions in expressions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jul 2008 12:25:12 -0400 |
parents | e86370850c30 |
children | 7bab29834cd6 |
line wrap: on
line diff
--- a/src/lacweb.grm Tue Jul 01 12:10:46 2008 -0400 +++ b/src/lacweb.grm Tue Jul 01 12:25:12 2008 -0400 @@ -196,6 +196,7 @@ | 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 @@ | 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))