mixfix operators [_.._] [_..] [.._] in WhyML as well

parent 2a7fc739
...@@ -762,6 +762,12 @@ expr_sub: ...@@ -762,6 +762,12 @@ expr_sub:
{ Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) } { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ | expr_arg LEFTSQ expr LARROW expr RIGHTSQ
{ Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) } { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
| expr_arg LEFTSQ expr DOTDOT expr RIGHTSQ
{ Eidapp (sub_op $startpos($2) $endpos($2), [$1;$3;$5]) }
| expr_arg LEFTSQ expr DOTDOT RIGHTSQ
{ Eidapp (above_op $startpos($2) $endpos($2), [$1;$3]) }
| expr_arg LEFTSQ DOTDOT expr RIGHTSQ
{ Eidapp (below_op $startpos($2) $endpos($2), [$1;$4]) }
loop_annotation: loop_annotation:
| (* epsilon *) | (* epsilon *)
......
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