Mercurial > urweb
diff src/lacweb.grm @ 82:b4f2a258e52c
Initial disjointness prover
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jul 2008 10:55:38 -0400 |
parents | 6431b315a1e3 |
children | 0a1baddd8ab2 |
line wrap: on
line diff
--- a/src/lacweb.grm Tue Jul 01 09:29:49 2008 -0400 +++ b/src/lacweb.grm Tue Jul 01 10:55:38 2008 -0400 @@ -40,7 +40,7 @@ | SYMBOL of string | CSYMBOL of string | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER - | CON | LTYPE | VAL | FOLD + | CON | LTYPE | VAL | FOLD | UNIT | KUNIT | TYPE | NAME | ARROW | LARROW | DARROW | FN | PLUSPLUS | DOLLAR @@ -179,6 +179,7 @@ | LBRACE kind RBRACE (KRecord kind, s (LBRACEleft, RBRACEright)) | kind ARROW kind (KArrow (kind1, kind2), s (kind1left, kind2right)) | LPAREN kind RPAREN (#1 kind, s (LPARENleft, RPARENright)) + | KUNIT (KUnit, s (KUNITleft, KUNITright)) | UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright)) capps : cterm (cterm) @@ -216,6 +217,7 @@ | path (CVar path, s (pathleft, pathright)) | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright)) | FOLD (CFold, s (FOLDleft, FOLDright)) + | UNIT (CUnit, s (UNITleft, UNITright)) rcon : ([]) | ident EQ cexp ([(ident, cexp)])