From 8b8129027d1408aa8a48184aa704349bf9cc6ceb Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 4 Dec 2023 23:35:54 +0100 Subject: [PATCH] update syntax.ebnf --- syntax.ebnf | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/syntax.ebnf b/syntax.ebnf index ff78604..1296129 100644 --- a/syntax.ebnf +++ b/syntax.ebnf @@ -24,7 +24,7 @@ dim arg = "@", dim. pat var = NAME | "_". -term = lambda | case | pi | sigma | ann. +term = lambda | pi | sigma | ann | let. lambda = ("λ" | "δ"), {pat var}+, "⇒", term. @@ -49,12 +49,18 @@ sigma = (binder | ann), "×", (sigma | ann). ann = infix eq, ["∷", term]. +bare let binder = pat var, "=", term. +qty let binder = [qty, "."], bare let binder. + +let = ("let0" | "let1" | "letω"), {bare let binder / ";"}+, "in", term + | "let", {qty let binder / ";"}+, "in", term. + infix eq = app term, ["≡", term, ":", app term]. (* dependent is below *) -app term = coe | comp | split universe | dep eq | succ | normal app. +app term = coe | comp | split universe | dep eq | special app | normal app. split universe = "★", NAT. dep eq = "Eq", type line, term arg, term arg. -succ = "succ", term arg. +special app = ("fst" | "snd" | "succ"), {term arg}+. normal app = term arg, {term arg | dim arg}. (* direction defaults to @0 @1 *) @@ -76,4 +82,5 @@ term arg = UNIVERSE | "★", SUPER | "zero" | NAT | QNAME, displacement - | "(", {term / ","}+, [","], ")". + | "(", {term / ","}+, [","], ")" + | case.