From 0a59ce43beaf13ec25a4483aaf7b8a66d9e4907e Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 12 Aug 2025 20:41:44 +0200
Subject: Relax function symbol definitions

Extra assumptions are simply discarded for now.
---
 source/Syntax/Concrete.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 3c6700b..8784a1f 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -255,10 +255,11 @@ grammar lexicon@Lexicon{..} = mdo
     defnHead <- rule $ optional _write *> asum [defnAdj, defnVerb, defnNoun, defnRel, defnSymbolicPredicate]
 
     defnIf <- rule $ Defn <$> asms <*> defnHead <* (_iff <|> _if) <*> stmt <* _dot
-    defnFunSymb <- rule $ _comma *> termExpr <* _comma --  ^ Optional symbolic equivalent.
+    defnFunSymb <- rule $ _comma *> termExpr <* _comma --  Optional symbolic equivalent.
     defnFun <- rule $ DefnFun <$> asms <*> (optional _the *> funVar) <*> optional defnFunSymb <* _is <*> term <* _dot
 
     symbolicPatternEqTerm <- rule do
+        asms -- NB assumptions are currently ignored!
         pat <- beginMath *> symbolicPattern <* _eq
         e <- expr <* endMath <* _dot
         pure (pat, e)
-- 
cgit v1.2.3