diff options
| -rw-r--r-- | library/topology/urysohn2.tex | 4 | ||||
| -rw-r--r-- | source/Checking.hs | 6 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 2 |
3 files changed, 7 insertions, 5 deletions
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 05ea180..f2f6ef3 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -46,7 +46,9 @@ Define $f : X \to \reals$ such that $f(x) = $ \begin{cases} - &(x + x) , x \in X + &(x + x) &\text{if} x \in X + & x &\text{if} x \neq \zero + & \zero & \text{if} x = \zero % & x ,x \in X <- will result in technicly ambigus parse \end{cases} 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' |