Revert "Parser: restore the old syntax for lambda-bindings in logical terms"

This reverts commit b19660c9.
We prefer not having two syntaxes for the same thing.
(With the approval of Andrei, of course.)
parent 6eccdac1
......@@ -187,8 +187,6 @@ rule token = parse
{ AND }
| "\\/"
{ OR }
| "\\"
{ LAMBDA }
| "."
{ DOT }
| ".."
......
......@@ -121,7 +121,7 @@
%token AND ARROW
%token BAR
%token COLON COMMA
%token DOT DOTDOT EQUAL LAMBDA LTGT
%token DOT DOTDOT EQUAL LTGT
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
%token LARROW LRARROW OR
%token RIGHTPAR RIGHTSQ
......@@ -153,7 +153,7 @@
%nonassoc LARROW
%nonassoc RIGHTSQ (* stronger than <- for e1[e2 <- e3] *)
%left OP2
%left OP3 LAMBDA
%left OP3
%left OP4
%nonassoc prec_prefix_op
%nonassoc LEFTSQ
......@@ -587,7 +587,6 @@ triggers:
quant:
| FORALL { Dterm.DTforall }
| EXISTS { Dterm.DTexists }
| LAMBDA { Dterm.DTlambda }
numeral:
| INTEGER { Number.ConstInt $1 }
......@@ -907,7 +906,6 @@ lident_op:
| op_symbol UNDERSCORE { prefix $1 }
| EQUAL { infix "=" }
| OPPREF { prefix $1 }
| LAMBDA { infix "\\" }
| LEFTSQ RIGHTSQ { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
......@@ -936,7 +934,6 @@ prefix_op:
| o = OP2 { mk_id (infix o) $startpos $endpos }
| o = OP3 { mk_id (infix o) $startpos $endpos }
| o = OP4 { mk_id (infix o) $startpos $endpos }
| LAMBDA { mk_id (infix "\\") $startpos $endpos }
(* Qualified idents *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment