From fab70aaf2947ff1369757355fbf11437c6db35ff Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Sun, 30 Jun 2024 15:07:02 +0200
Subject: implement syntax for non-dependent function and pair types

---
 src/parser/Grammar.mly | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/parser')

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
-- 
cgit 1.4.1