From ce03d33eaa7e9d37935f225d48459223a4004a50 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 24 Aug 2024 19:30:46 +0200
Subject: First atemped to write a new way of local function defintion

---
 source/Syntax/Abstract.hs | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'source/Syntax/Abstract.hs')

diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 4aa8623..f775b69 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -369,6 +369,13 @@ data Proof
     -- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/.
     -- The first 'VarSymbol' is the newly defined symbol, the second one is the argument.
     -- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function).
+    
+    
+    
+    
+    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol [VarSymbol Expr [VarSymbol] Expr ] Proof
+    -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
+    -- 
     deriving (Show, Eq, Ord)
 
 -- | An inline justification.
-- 
cgit v1.2.3


From d79c85d70fc907858e3af5715bb94e8fdc202155 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 26 Aug 2024 15:33:04 +0200
Subject: I implemented a parsing rule in concrete.hs for local functions and a
 abstract type in abstract.hs for the proof data structure.

---
 source/Syntax/Abstract.hs |  2 +-
 source/Syntax/Concrete.hs | 36 ++++++++++++++++++++++--------------
 2 files changed, 23 insertions(+), 15 deletions(-)

(limited to 'source/Syntax/Abstract.hs')

diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index f775b69..6457d42 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -373,7 +373,7 @@ data Proof
     
     
     
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol [VarSymbol Expr [VarSymbol] Expr ] Proof
+    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty [(Expr, Formula)]) Proof
     -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
     -- 
     deriving (Show, Eq, Ord)
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 51cc013..f414ea6 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -354,17 +354,36 @@ grammar lexicon@Lexicon{..} = mdo
     
 
 
+
+
+
     -- Define $f $\fromTo{X}{Y} such that,         
     -- Define function $f: X \to Y$,
     -- \begin{align}
     --      &x \mapsto 3*x      &,  
-    --      &x \mapsto 4*k+x    &, 
+    --      &x \mapsto 4*k    &,    \forall k \in \N. x \in \Set{k}
     -- \end{align}
     -- 
+
+    -- Follwing is the definition right now.
+    -- Define function $f: X \to Y$ such that,
+    -- \begin{cases}
+    --     1 & \text{if } x \in \mathbb{Q}\\
+    --     0 & \text{if } x \in \mathbb{R}\setminus\mathbb{Q}
+    --     3 & \text{else}     
+    -- \end{cases}
+
+    functionDefineCase <- rule $ (:[]) <$> ((,) <$> expr <*> (_ampersand *> formula))
     defineFunctionMathy <-  rule    $ DefineFunctionMathy 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
-                                    <*> _colon *> varSymbol <*> _to *> varSymbol      -- : 'var' \to 'var'
-                                    <*> localFunctionDefinitionAlign 
+                                    <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
+                                    <*> (_to *> varSymbol <* endMath <* _suchThat) 
+                                    -- <*> (_suchThat  *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula))))
+                                    -- <*> (_suchThat  *> align (many1 (varSymbol <* exprApp <*  formula)))
+                                    <*> varSymbol <*> varSymbol <* symbol "="
+                                    <*> many1 functionDefineCase
+                                    <*> proof 
+
 
 
     proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed]
@@ -450,17 +469,6 @@ enumeratedMarked1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token
 enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> label) <*> p) <* end "enumerate" <?> "\"\\begin{enumerate}\\item\\label{...}...\""
 
 
--- &x \mapsto 'someexpr'  &, for x
-localFunctionDefinitionAlign :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Marker, a)
-localFunctionDefinitionAlign p =    begin "align" *> many1 funDefExp <* end "align" 
-                                    <?> "\"\\begin{algin} &x \\mapsto x+2 , x \\in X \\ \\end{algin}\""
-
-
-funDefExp :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [(Marker, a)]
-funDefExp p = NonEmpty.toList <$> ( _ampersand *> varSymbol <*> funDefExpRange <*> (_ampersand *> varSymbol <* _in) <*> varSymbol) -- the last var should be a expression
-
-funDefRange :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty (Marker, a))
-funDefRange p = _mapsto *> varSymbol -- TODO: this Var has to be changed to a expression
 
 -- This function could be rewritten, so that it can be used directly in the grammar,
 -- instead of with specialized variants.
-- 
cgit v1.2.3


From 76ea8e11d943b123d28dfbe2f354838f80fb8dba Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 26 Aug 2024 20:14:18 +0200
Subject: Implemented the checking for local functions.

---
 source/Checking.hs        | 39 ++++++++++++++++++++++++++++++++++++++-
 source/Meaning.hs         | 12 +++++-------
 source/Syntax/Abstract.hs |  2 +-
 source/Syntax/Adapt.hs    |  2 +-
 source/Syntax/Concrete.hs |  2 +-
 source/Syntax/Internal.hs |  2 +-
 6 files changed, 47 insertions(+), 12 deletions(-)

(limited to 'source/Syntax/Abstract.hs')

diff --git a/source/Checking.hs b/source/Checking.hs
index dc90264..817c477 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -28,6 +28,7 @@ import Data.HashSet qualified as HS
 import Data.InsOrdMap (InsOrdMap)
 import Data.InsOrdMap qualified as InsOrdMap
 import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
 import Data.Set qualified as Set
 import Data.Text qualified as Text
 import Data.Text.IO qualified as Text
@@ -149,7 +150,7 @@ assume asms = traverse_ go asms
         go :: Asm -> Checking
         go = \case
             Asm phi -> do
-                phi' <-  (canonicalize phi)
+                phi' <- canonicalize phi
                 modify \st ->
                     st{ checkingAssumptions = phi' : checkingAssumptions st
                     , fixedVars = freeVars phi' <> fixedVars st
@@ -542,6 +543,42 @@ checkProof = \case
         checkCalc calc
         assume [Asm (calcResult calc)]
         checkProof continue
+    DefineFunctionMathy funVar domVar ranVar argVar definitions continue -> do
+        -- We have f: X \to Y and x \mapsto ...  
+        -- definition is a nonempty list of (expresssion e, formula phi)
+        -- such that f(x) =  e if phi(x)
+        -- since we do a case deduction in the definition there has to be a check that,
+        -- our domains in the case are a disjunct union of dom(f)
+        assume 
+            [Asm (TermOp DomSymbol [TermVar funVar] `Equals` TermVar domVar)
+            ,Asm (rightUniqueAdj (TermVar funVar))
+            ,Asm (relationNoun (TermVar funVar))]
+
+        goals <- gets checkingGoals
+        setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union
+        tellTasks
+
+        assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` TermVar ranVar)))] -- function f from \dom(f) \to \ran(f)
+        assume (functionSubdomianExpression funVar argVar definitions) --behavior on the subdomians
+        setGoals goals
+        checkProof continue
+
+
+-- | Makes a conjunction of all the subdomain statments
+subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula 
+subdomainConjuctionLocalFunction argVar defintions = 
+    let stmts = [snd x | x <- NonEmpty.toList defintions]
+    in TermVar argVar `IsElementOf` makeConjunction stmts
+
+
+functionSubdomianExpression :: VarSymbol -> VarSymbol -> NonEmpty (Term, Formula) -> [Asm]
+functionSubdomianExpression f a nxs = case nxs of
+    x:|xs -> singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a (NonEmpty.fromList xs)
+    
+
+singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> (Term, Formula) -> Asm
+singleFunctionSubdomianExpression funVar argVar x = Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` snd x) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` fst x)))
+
 
 checkCalc :: Calc -> Checking
 checkCalc calc = locally do
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 30e13f8..ab98c9a 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -607,17 +607,15 @@ glossProof = \case
             else error "mismatched variables in function definition."
     
     Raw.DefineFunctionMathy funVar domVar ranVar funVar2 argVar definitions proof -> do
-        if funVar /= funVar2
-            then error "missmatched function names"
-            else Sem.DefineFunctionMathy funVar domVar ranVar argVar <*> glossLocalFunctionExprEach definitions <*> glossProof proof
+        if funVar == funVar2
+            then Sem.DefineFunctionMathy funVar domVar ranVar argVar <$> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
+            else error "missmatched function names"
     Raw.Calc calc proof ->
         Sem.Calc <$> glossCalc calc <*> glossProof proof
 
-glossLocalFunctionExprEach :: NonEmpty [(Raw.Expr, Raw.Formula)]-> Gloss [(Sem.Term, Sem.Formula)]
-glossLocalFunctionExprEach def = pure ( glossLocalFunctionExpr `each` def )
 
-glossLocalFunctionExpr :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula)
-glossLocalFunctionExpr (definingExpression, localDomain) = do
+glossLocalFunctionExprDef :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula)
+glossLocalFunctionExprDef (definingExpression, localDomain) = do
     e <- glossExpr definingExpression
     d <- glossFormula localDomain
     pure (e,d)
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 6457d42..6372c87 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -373,7 +373,7 @@ data Proof
     
     
     
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty [(Expr, Formula)]) Proof
+    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
     -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
     -- 
     deriving (Show, Eq, Ord)
diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index 96fd76d..3cff497 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -35,7 +35,7 @@ scanChunk ltoks =
         Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ ->
             matchOrErr inductive "inductive definition" pos
         Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ ->
-            matchOrErr signature "signature" pos
+            matchOrErr signatureIntro "signature" pos
         _ -> []
 
 adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index f414ea6..69280c1 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 $ (:[]) <$> ((,) <$> expr <*> (_ampersand *> formula))
+    functionDefineCase <- rule $ (,) <$> expr <*> (_ampersand *> formula)
     defineFunctionMathy <-  rule    $ DefineFunctionMathy 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
                                     <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 872ae06..0e3361d 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -436,7 +436,7 @@ data Proof
     | Define VarSymbol Term Proof
     | DefineFunction VarSymbol VarSymbol Term Term Proof
 
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol [(Term, Formula)] Proof
+    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Term, Formula)) Proof
 
 deriving instance Show Proof
 deriving instance Eq   Proof
-- 
cgit v1.2.3


From 30f7c63ce566c993816607f3368c357233693aae Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 27 Aug 2024 01:44:45 +0200
Subject: Experimental working commit, programm will compile But the Proof that
 the domain of the local function is not right. Also if in the definition of
 our local function we just use f(x) = x then we get a technical ambigus parse

---
 library/topology/urysohn2.tex |  8 ++++++--
 source/Checking.hs            | 13 +++++++------
 source/Meaning.hs             |  4 ++--
 source/Syntax/Abstract.hs     |  2 +-
 source/Syntax/Adapt.hs        |  4 ++--
 source/Syntax/Concrete.hs     | 13 ++++++++-----
 source/Syntax/Internal.hs     |  2 +-
 source/Syntax/Token.hs        | 17 +++++++++++++++--
 8 files changed, 42 insertions(+), 21 deletions(-)

(limited to 'source/Syntax/Abstract.hs')

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 8e5261e..05ea180 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -44,10 +44,14 @@
 \begin{proof}
 
 
+    Define $f : X \to \reals$ such that  $f(x) = $
+    \begin{cases}
+        &(x + x) , x \in X
+        % & x ,x \in X    <- will result in technicly ambigus parse
+    \end{cases}
 
-
+    Trivial.
     
-    Contradiction.
     
 \end{proof}
 
diff --git a/source/Checking.hs b/source/Checking.hs
index 817c477..6d55ee1 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -543,7 +543,7 @@ checkProof = \case
         checkCalc calc
         assume [Asm (calcResult calc)]
         checkProof continue
-    DefineFunctionMathy funVar domVar ranVar argVar definitions continue -> do
+    DefineFunctionMathy funVar argVar domVar ranExpr definitions continue -> do
         -- We have f: X \to Y and x \mapsto ...  
         -- definition is a nonempty list of (expresssion e, formula phi)
         -- such that f(x) =  e if phi(x)
@@ -558,8 +558,8 @@ checkProof = \case
         setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union
         tellTasks
 
-        assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` TermVar ranVar)))] -- function f from \dom(f) \to \ran(f)
-        assume (functionSubdomianExpression funVar argVar definitions) --behavior on the subdomians
+        assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f)
+        assume (functionSubdomianExpression funVar argVar (NonEmpty.toList definitions)) --behavior on the subdomians
         setGoals goals
         checkProof continue
 
@@ -571,9 +571,10 @@ subdomainConjuctionLocalFunction argVar defintions =
     in TermVar argVar `IsElementOf` makeConjunction stmts
 
 
-functionSubdomianExpression :: VarSymbol -> VarSymbol -> NonEmpty (Term, Formula) -> [Asm]
-functionSubdomianExpression f a nxs = case nxs of
-    x:|xs -> singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a (NonEmpty.fromList xs)
+functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
+functionSubdomianExpression f a (x:xs) = singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a xs
+functionSubdomianExpression _ _ [] = []
+
     
 
 singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> (Term, Formula) -> Asm
diff --git a/source/Meaning.hs b/source/Meaning.hs
index ab98c9a..4a21fa3 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -606,9 +606,9 @@ glossProof = \case
             then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
             else error "mismatched variables in function definition."
     
-    Raw.DefineFunctionMathy funVar domVar ranVar funVar2 argVar definitions proof -> do
+    Raw.DefineFunctionMathy funVar domVar ranExpr funVar2 argVar definitions proof -> do
         if funVar == funVar2
-            then Sem.DefineFunctionMathy funVar domVar ranVar argVar <$> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
+            then Sem.DefineFunctionMathy funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
             else error "missmatched function names"
     Raw.Calc calc proof ->
         Sem.Calc <$> glossCalc calc <*> glossProof proof
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 6372c87..13691e7 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -373,7 +373,7 @@ data Proof
     
     
     
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
+    | DefineFunctionMathy VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
     -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
     -- 
     deriving (Show, Eq, Ord)
diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index 3cff497..4b43bc6 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -34,8 +34,8 @@ scanChunk ltoks =
             matchOrErr struct "struct definition" pos
         Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ ->
             matchOrErr inductive "inductive definition" pos
-        Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ ->
-            matchOrErr signatureIntro "signature" pos
+        --Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ ->
+        --    matchOrErr signatureIntro "signature" pos
         _ -> []
 
 adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 69280c1..fe08fec 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -373,16 +373,16 @@ grammar lexicon@Lexicon{..} = mdo
     --     3 & \text{else}     
     -- \end{cases}
 
-    functionDefineCase <- rule $ (,) <$> expr <*> (_ampersand *> formula)
+    functionDefineCase <- rule $ (,) <$> (_ampersand *> (expr <|> exprVar )) <*> (_comma *> formula)
     defineFunctionMathy <-  rule    $ DefineFunctionMathy 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
                                     <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
-                                    <*> (_to *> varSymbol <* endMath <* _suchThat) 
+                                    <*> (_to *> expr <* endMath <* _suchThat) 
                                     -- <*> (_suchThat  *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula))))
                                     -- <*> (_suchThat  *> align (many1 (varSymbol <* exprApp <*  formula)))
-                                    <*> varSymbol <*> varSymbol <* symbol "="
-                                    <*> many1 functionDefineCase
-                                    <*> proof 
+                                    <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq <* endMath)
+                                    <*> cases (many1 functionDefineCase)
+                                    <*> proof
 
 
 
@@ -644,6 +644,9 @@ group body = token InvisibleBraceL *> body <* token InvisibleBraceR <?> "\"{...}
 align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
 align body = begin "align*" *> body <* end "align*"
 
+cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+cases body = begin "cases" *> body <* end "cases"
+
 
 maybeVarToken :: Located Token -> Maybe VarSymbol
 maybeVarToken ltok = case unLocated ltok of
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 0e3361d..7046161 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -436,7 +436,7 @@ data Proof
     | Define VarSymbol Term Proof
     | DefineFunction VarSymbol VarSymbol Term Term Proof
 
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Term, Formula)) Proof
+    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
 
 deriving instance Show Proof
 deriving instance Eq   Proof
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index cb3f4cb..52da86a 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -189,6 +189,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:))
                 Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:))
+                Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:))
                 Just t -> goNormal (f . (t:))
         goText f = do
             r <- optional textToken
@@ -204,6 +205,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:))
                 Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:))
+                Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:))
                 Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:))
                 Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:))
                 Just t -> goMath (f . (t:))
@@ -219,12 +221,12 @@ toks = whitespace *> goNormal id <* eof
 -- | Parses a single normal mode token.
 tok :: Lexer (Located Token)
 tok =
-    word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command
+    word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> casesBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command
 
 -- | Parses a single math mode token.
 mathToken :: Lexer (Located Token)
 mathToken =
-    var <|> symbol <|> number <|> begin <|> alignEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command
+    var <|> symbol <|> number <|> begin <|> alignEnd <|> casesEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command
 
 beginText :: Lexer (Located Token)
 beginText = lexeme do
@@ -277,6 +279,11 @@ alignBegin = guardM isTextMode *> lexeme do
     setMathMode
     pure (BeginEnv "align*")
 
+casesBegin :: Lexer (Located Token)
+casesBegin = guardM isTextMode *> lexeme do
+    Char.string "\\begin{cases}"
+    setMathMode
+    pure (BeginEnv "cases")
 
 -- | Parses a single end math token.
 mathEnd :: Lexer (Located Token)
@@ -291,6 +298,12 @@ alignEnd = guardM isMathMode *> lexeme do
     setTextMode
     pure (EndEnv "align*")
 
+casesEnd :: Lexer (Located Token)
+casesEnd = guardM isMathMode *> lexeme do
+    Char.string "\\end{cases}"
+    setTextMode
+    pure (EndEnv "cases")
+
 
 -- | Parses a word. Words are returned casefolded, since we want to ignore their case later on.
 word :: Lexer (Located Token)
-- 
cgit v1.2.3


From c943ca6441e9118bc9caee1c11f697da89bc06b7 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 18 Sep 2024 00:01:42 +0200
Subject: working commit

---
 library/set/equinumerosity.tex |   2 +-
 library/topology/urysohn2.tex  | 260 ++++++++++++++++++++++++++++++++++++++---
 source/Checking.hs             |   2 +-
 source/Meaning.hs              |   4 +-
 source/Syntax/Abstract.hs      |   2 +-
 source/Syntax/Concrete.hs      |   4 +-
 source/Syntax/Internal.hs      |   2 +-
 7 files changed, 250 insertions(+), 26 deletions(-)

(limited to 'source/Syntax/Abstract.hs')

diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex
index a846b78..a922052 100644
--- a/library/set/equinumerosity.tex
+++ b/library/set/equinumerosity.tex
@@ -15,7 +15,7 @@
     $A\approx A$.
 \end{proposition}
 \begin{proof}
-    $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_is_bijection}.
+    $\identity{A}$ is a bijection from $A$ to $A$. %by \cref{id_is_bijection}.
     Follows by \cref{equinum}.
 \end{proof}
 
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 9990199..97bbc70 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -13,6 +13,7 @@
 \import{set/fixpoint.tex}
 \import{set/product.tex}
 \import{topology/real-topological-space.tex}
+\import{set/equinumerosity.tex}
 
 \section{Urysohns Lemma}
 
@@ -251,6 +252,7 @@
 
 
 
+
 \begin{proposition}\label{naturals_leq_on_suc}
     For all $n,m \in \naturals$ such that $m < \suc{n}$ we have $m \leq n$.
 \end{proposition}
@@ -358,6 +360,218 @@
     Omitted.
 \end{proof}
 
+\begin{lemma}\label{naturals_suc_injective}
+    Suppose $n,m \in \naturals$.
+    $n = m$ iff $\suc{n} = \suc{m}$.
+\end{lemma}
+
+\begin{lemma}\label{naturals_rless_implies_not_eq}
+    Suppose $n,m \in \naturals$.
+    Suppose $n < m$.
+    Then $n \neq m$.
+\end{lemma}
+
+\begin{lemma}\label{cardinality_of_singleton}
+    For all $x$ such that $x \neq \emptyset$ we have $\{x\}$ has cardinality $1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+    %Fix $x$.
+    %Suppose $x \neq \emptyset$.
+    %Let $X = \{x\}$.
+    %$\seq{\zero}{\zero}=1$.
+    %$\seq{\zero}{\zero}$ has cardinality $1$.
+    %$X \setminus \{x\} = \emptyset$.
+    %$1 = \{\emptyset\}$.
+    %Let $F = \{(x,\emptyset)\}$.
+    %$F$ is a relation.
+    %$\dom{F} = X$.
+    %$\emptyset \in \ran{F}$.
+    %for all $x \in 1$ we have $x = \emptyset$.
+    %$\ran{F} = 1$.
+    %$F$ is injective.
+    %$F \in \surj{X}{1}$.
+    %$F$ is a bijection from $X$ to $1$.
+\end{proof}
+
+\begin{lemma}\label{cardinality_n_plus_1}
+    For all $n \in \naturals$ we have $n+1$ has cardinality $n+1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{cardinality_n_m_plus}
+    For all $n,m \in \naturals$ we have $n+m$ has cardinality $n+m$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{cardinality_plus_disjoint}
+    Suppose $X \inter Y = \emptyset$.
+    Suppose $X$ is finite.
+    Suppose $Y$ is finite.
+    Suppose $X$ has cardinality $n$.
+    Suppose $Y$ has cardinality $m$.
+    Then $X \union Y$ has cardinality $m+n$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+
+\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1}
+    Suppose $f$ is a bijection from $X$ to $Y$.
+    Suppose $g$ is a function from $X$ to $Y$.
+    Suppose $g$ is injective.
+    Suppose $X$ is finite and $Y$ is finite. 
+    For all $n \in \naturals$ such that $Y$ has cardinality $n$ we have $g$ is a bijection from $X$ to $Y$.
+\end{lemma}
+\begin{proof}[Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    Suppose $Y$ has cardinality $n$.
+    $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,notin_emptyset}.
+    \begin{byCase}
+        \caseOf{$n = \zero$.} 
+            Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}.
+        \caseOf{$n \neq \zero$.}
+            %Take $n' \in n$ such that $n = \suc{n'}$.
+            %$n' \in \naturals$.
+            %$n' + 1 = n$.
+            %Take $y$ such that $y \in Y$ by \cref{funs_type_apply,apply,bijections_to_funs,cardinality,foundation}. 
+            %Let $Y' = Y \setminus \{y\}$.
+            %$Y' \subseteq Y$.
+            %$Y'$ is finite.
+            %There exist $m \in \naturals$ such that $Y'$ has cardinality $m$.
+            %Take $m \in \naturals$ such that $Y'$ has cardinality $m$.
+            %Then $Y'$ has cardinality $n'$.
+            %Let $x' = \apply{\converse{f}}{y'}$. 
+            %$x' \in X$.
+            %Let $X' = X \setminus \{x'\}$.
+            %$X' \subseteq X$.
+            %$X'$ is finite.
+            %There exist $m' \in \naturals$ such that $X'$ has cardinality $m'$.
+            %Take $m' \in \naturals$ such that $X''$ has cardinality $m'$.
+            %Then $X'$ has cardinality $n'$.
+            %Let $f'(z)=f(z)$ for $z \in X'$.
+            %$\dom{f'} = X'$.
+            %$\ran{f'} = Y'$.
+            %$f'$ is a bijection from $X'$ to $Y'$.
+            %Let $g'(z) = g(z)$ for $z \in X'$.
+            %Then $g'$ is injective.
+            %Then $g'$ is a bijection from $X'$ to $Y'$ by \cref{rels,id_elem_rels,times_empty_right,powerset_emptyset,double_complement_union,unions_cons,union_eq_cons,union_as_unions,unions_pow,cons_absorb,setminus_self,bijections_dom,ran_converse,id_apply,apply,unions_emptyset,img_emptyset,zero_is_empty}.
+            %Define $G : X \to Y$ such that $G(z)=
+            %\begin{cases}
+            %    g'(z) & \text{if} z \in X' \\
+            %    y' & \text{if} z = x'
+            %\end{cases}$
+            %$G = g$.
+            %Follows by \cref{double_relative_complement,fun_to_surj,bijections,funs_surj_iff,bijections_to_funs,neq_witness,surj,funs_elim,setminus_self,cons_subseteq_iff,cardinality,ordinal_empty_or_emptyset_elem,naturals_inductive_set,natural_number_is_ordinal_for_all,foundation,inter_eq_left_implies_subseteq,inter_emptyset,cons_subseteq_intro,emptyset_subseteq}.
+            Omitted.
+    \end{byCase}
+    %$\converse{f}$ is a bijection from $Y$ to $X$.
+    %Let $h = g \circ \converse{f}$.
+    %It suffices to show that $\ran{g} = Y$ by \cref{fun_to_surj,dom_converse,bijections}.
+    %It suffices to show that for all $y \in Y$ we have there exist $x \in X$ such that $g(x)=y$ by \cref{funs_ran,subseteq_antisymmetric,fun_ran_iff,apply,funs_elim,ran_converse,subseteq}.
+%
+    %Fix $y \in Y$.
+    %Take $x \in X$ such that $\apply{\converse{f}}{y} = x$.
+
+\end{proof}
+
+\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection}
+    Suppose $f$ is a bijection from $X$ to $Y$.
+    Suppose $g$ is a function from $X$ to $Y$.
+    Suppose $g$ is injective.
+    Suppose $Y$ is finite. 
+    Then $g$ is a bijection from $X$ to $Y$.
+\end{lemma}
+\begin{proof}
+    There exist $n \in \naturals$ such that $Y$ has cardinality $n$ by \cref{cardinality,injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,finite}.
+    Follows by \cref{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,cardinality,equinum_tran,equinum_sym,equinum,finite}.
+\end{proof}
+
+
+
+\begin{lemma}\label{naturals_bijection_implies_eq}
+    Suppose $n,m \in \naturals$.
+    Suppose $f$ is a bijection from $n$ to $m$.
+    Then $n = m$.
+\end{lemma}
+\begin{proof}
+    $n$ is finite.
+    $m$ is finite.
+    Suppose not.
+    Then $n < m$ or $m < n$.
+    \begin{byCase}
+        \caseOf{$n < m$.}
+            Then $n \in m$.
+            There exist $x \in m$ such that $x \notin n$.
+            $\identity{n}$ is a function from $n$ to $m$.
+            $\identity{n}$ is injective.
+            $\apply{\identity{n}}{n} = n$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}.
+            Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}.
+        \caseOf{$m < n$.}
+            Then $m \in n$.
+            There exist $x \in n$ such that $x \notin m$.
+            $\converse{f}$ is a bijection from $m$ to $n$.
+            $\identity{m}$ is a function from $m$ to $n$.
+            $\identity{m}$ is injective.
+            $\apply{\identity{m}}{m} = m$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}.
+            Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}.
+    \end{byCase}
+\end{proof}
+
+\begin{lemma}\label{naturals_eq_iff_bijection}
+    Suppose $n,m \in \naturals$.
+    $n = m$ iff there exist $f$ such that $f$ is a bijection from $n$ to $m$.
+\end{lemma}
+\begin{proof}
+    We show that if $n = m$ then there exist $f$ such that $f$ is a bijection from $n$ to $m$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+    We show that for all $k \in \naturals$ we have if there exist $f$ such that $f$ is a bijection from $k$ to $m$ then $k = m$.
+    \begin{subproof}%[Proof by \in-induction on $k$]
+        %Assume $k \in \naturals$.
+        %\begin{byCase}
+        %    \caseOf{$k = \zero$.} 
+        %        Trivial.
+        %    \caseOf{$k \neq \zero$.}
+        %        \begin{byCase}
+        %            \caseOf{$m = \zero$.}
+        %                Trivial.
+        %            \caseOf{$m \neq \zero$.}
+        %                Take $k' \in \naturals$ such that $\suc{k'} = k$.
+        %                Then $k' \in k$.
+        %                Take $m' \in \naturals$ such that $m = \suc{m'}$.
+        %                Then $m' \in m$.
+        %                
+        %        \end{byCase}
+        %\end{byCase}
+    \end{subproof}
+\end{proof}
+
+\begin{lemma}\label{seq_from_zero_suc_cardinality_eq_upper_border}
+    Suppose $n,m \in \naturals$.
+    Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$.
+    Then $n = m$.
+\end{lemma}
+\begin{proof}
+    We have $\seq{\zero}{n} = \suc{n}$.
+    Take $f$ such that $f$ is a bijection from $\seq{\zero}{n}$ to $\suc{m}$.
+    Therefore $n=m$ by \cref{suc_injective,naturals_inductive_set,cardinality,naturals_eq_iff_bijection}.
+\end{proof}
+
+\begin{lemma}\label{seq_from_zero_cardinality_eq_upper_border_set_eq}
+    Suppose $n,m \in \naturals$.
+    Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$.
+    Then $\seq{\zero}{n} = \seq{\zero}{m}$.
+\end{lemma}
+
 \begin{proposition}\label{existence_normal_ordered_urysohn}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain of $X$.
@@ -384,23 +598,24 @@
                 Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
                 Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
                 $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}.
-                We show that $\seq{\zero}{k'} = \seq{\zero}{k}$.
-                \begin{subproof}
-                    We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$.
-                    \begin{subproof}
-                        It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$.
-                        Fix $y \in \seq{\emptyset}{k'}$.
-                        Then $y \leq k'$.
-                        Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}.
-                        %Then $\seq{\emptyset}{k'} \in \suc{k}$.
-                        Therefore $y \in \suc{k}$.
-                        Therefore $y \in \seq{\emptyset}{k}$.
-                    \end{subproof}
-                    We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$.
-                    \begin{subproof}
-                        Fix $y \in \seq{\emptyset}{k}$.
-                    \end{subproof}
-                \end{subproof}
+                $\seq{\zero}{k'} = \seq{\zero}{k}$ by \cref{omega_is_an_ordinal,seq_from_zero_cardinality_eq_upper_border_set_eq,suc_subseteq_implies_in,suc_subseteq_elim,ordinal_suc_subseteq,cardinality}.
+                %We show that $\seq{\zero}{k'} = \seq{\zero}{k}$.
+                %\begin{subproof}
+                %    We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$.
+                %    \begin{subproof}
+                %        It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$.
+                %        Fix $y \in \seq{\emptyset}{k'}$.
+                %        Then $y \leq k'$.
+                %        Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}.
+                %        
+                %        Therefore $y \in \suc{k}$.
+                %        Therefore $y \in \seq{\emptyset}{k}$.
+                %    \end{subproof}
+                %    We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$.
+                %    \begin{subproof}
+                %        Fix $y \in \seq{\emptyset}{k}$.
+                %    \end{subproof}
+                %\end{subproof}
             \end{subproof}
             Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
             Let $N = \seq{\zero}{k}$.
@@ -452,7 +667,9 @@
     $f$ is staircase sequence of $U$ iff $f$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{f}$ and for all $n \in \dom{U}$ we have $\at{f}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$.
 \end{definition}
 
-
+\begin{definition}
+    
+\end{definition}
 
 
 
@@ -565,8 +782,15 @@
     \end{subproof}
     Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$.
 
+    We show that there exist $S$ such that $S$ is staircase sequence of $U$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    Take $S$ such that $S$ is staircase sequence of $U$.
 
+    For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$.
 
+    We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for .
 
 
     
diff --git a/source/Checking.hs b/source/Checking.hs
index 766c327..8bc38a4 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -543,7 +543,7 @@ checkProof = \case
         checkCalc calc
         assume [Asm (calcResult calc)]
         checkProof continue
-    DefineFunctionMathy funVar argVar domVar ranExpr definitions continue -> do
+    DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do
         -- We have f: X \to Y and x \mapsto ...  
         -- definition is a nonempty list of (expresssion e, formula phi)
         -- such that f(x) =  e if phi(x)
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 4a21fa3..00a944f 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -606,9 +606,9 @@ glossProof = \case
             then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
             else error "mismatched variables in function definition."
     
-    Raw.DefineFunctionMathy funVar domVar ranExpr funVar2 argVar definitions proof -> do
+    Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do
         if funVar == funVar2
-            then Sem.DefineFunctionMathy funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
+            then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
             else error "missmatched function names"
     Raw.Calc calc proof ->
         Sem.Calc <$> glossCalc calc <*> glossProof proof
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 13691e7..c8022c7 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -373,7 +373,7 @@ data Proof
     
     
     
-    | DefineFunctionMathy VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
+    | DefineFunctionLocal VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
     -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
     -- 
     deriving (Show, Eq, Ord)
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 7a89bea..9b947b0 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -374,7 +374,7 @@ grammar lexicon@Lexicon{..} = mdo
     -- \end{cases}
 
     functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula)
-    defineFunctionMathy <-  rule    $ DefineFunctionMathy 
+    defineFunctionLocal <-  rule    $ DefineFunctionLocal 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
                                     <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
                                     <*> (_to *> expr <* endMath <* _suchThat) 
@@ -386,7 +386,7 @@ grammar lexicon@Lexicon{..} = mdo
 
 
 
-    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed]
+    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionLocal, qed]
 
 
     blockAxiom  <- rule $ uncurry3 BlockAxiom     <$> envPos  "axiom" axiom
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index e83126d..c098380 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -446,7 +446,7 @@ data Proof
     | Define VarSymbol Term Proof
     | DefineFunction VarSymbol VarSymbol Term Term Proof
 
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
+    | DefineFunctionLocal VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
 
 deriving instance Show Proof
 deriving instance Eq   Proof
-- 
cgit v1.2.3