From 604d7a87b4c45ab13ef03e3c7a611ad4f9342f23 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 27 Aug 2024 02:13:29 +0200
Subject: ambigus parse fix. The proof goal must be changed, since now some
 could define a function with overlapping and worng subdomains

---
 source/Checking.hs        | 6 +++---
 source/Syntax/Concrete.hs | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'source')

diff --git a/source/Checking.hs b/source/Checking.hs
index 6d55ee1..7362c93 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -564,11 +564,11 @@ checkProof = \case
         checkProof continue
 
 
--- | Makes a conjunction of all the subdomain statments
+-- | Makes a conjunction of all the subdomain statments <- this has to be checked!!!! TODO!!!!!!
 subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula 
-subdomainConjuctionLocalFunction argVar defintions = 
+subdomainConjuctionLocalFunction _ defintions = 
     let stmts = [snd x | x <- NonEmpty.toList defintions]
-    in TermVar argVar `IsElementOf` makeConjunction stmts
+    in makeDisjunction stmts 
 
 
 functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index fe08fec..9d52995 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -373,7 +373,7 @@ grammar lexicon@Lexicon{..} = mdo
     --     3 & \text{else}     
     -- \end{cases}
 
-    functionDefineCase <- rule $ (,) <$> (_ampersand *> (expr <|> exprVar )) <*> (_comma *> formula)
+    functionDefineCase <- rule $ (,) <$> (_ampersand *> expr) <*> (_ampersand *> text _if *> formula)
     defineFunctionMathy <-  rule    $ DefineFunctionMathy 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
                                     <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
-- 
cgit v1.2.3