aya: upgrade with match elim syntax

aya-prover · Dec 12, 2024 · c42ab2b · c42ab2b
1 parent b576883
commit c42ab2b
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/main/grammar/AyaPsiParser.bnf b/src/main/grammar/AyaPsiParser.bnf
@@ -67,6 +67,7 @@
     KW_HIDING = 'hiding'
     KW_MODULE = 'module'
     KW_MATCH = 'match'
+    KW_RETURNS = 'returns'
     KW_VARIABLE = 'variable'
     KW_DEF = 'def'
     KW_CLASS = 'class'
@@ -287,7 +288,7 @@ piExpr ::= KW_PI tele+ TO expr
 forallExpr ::= KW_FORALL lambdaTele+ TO expr
 sigmaExpr ::= KW_SIGMA tele+ SUCHTHAT expr
 lambdaExpr ::= KW_LAMBDA teleBinderUntyped (IMPLIES expr)?
-matchExpr ::= KW_MATCH exprList clauses
+matchExpr ::= KW_MATCH KW_ELIM? exprList matchType? clauses
 doExpr ::= KW_DO LBRACE? <<commaSep doBlockContent>> RBRACE?
 selfExpr ::= KW_SELF (AT qualifiedId)?
 letBind ::= weakId lambdaTele* type? DEFINE_AS expr {
@@ -299,6 +300,8 @@ letExpr ::= KW_LET (KW_OPEN qualifiedId useHide? | letBindBlock) KW_IN expr
 
 doBlockContent ::= doBinding | expr
 
+matchType ::= (KW_AS <<commaSep weakId>>)? KW_RETURNS expr
+
 argument ::= atomExArgument
            | tupleImArgument
            | namedImArgument