aboutsummaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/Grammar.mly4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/Grammar.mly b/src/parser/Grammar.mly
index bb98029..d8e9ee0 100644
--- a/src/parser/Grammar.mly
+++ b/src/parser/Grammar.mly
@@ -47,6 +47,8 @@ raw_expr:
| a = arg; ARROW; b = expr
{ Pi (a, b) }
+ | a = expr; ARROW; b = expr
+ { Fun (a, b) }
| BACKSLASH; a = local_name; ARROW; b = expr
{ Lam (a, b) }
| a = expr; b = expr %prec APP
@@ -54,6 +56,8 @@ raw_expr:
| a = arg; ASTERISK; b = expr
{ Sg (a, b) }
+ | a = expr; ASTERISK; b = expr
+ { Prod (a, b) }
| LPR; a = expr; COMMA; b = expr; RPR
{ Pair (a, b) }
| FST; p = expr