From b71f135d5762f2a12bf08c71ecdcd221ed87cff0 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 6 Jul 2024 19:22:03 +0200
Subject: Formalisation of integers.

---
 source/Syntax/Lexicon.hs | 1 +
 1 file changed, 1 insertion(+)

(limited to 'source/Syntax')

diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
index 463dd18..65072ee 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Syntax/Lexicon.hs
@@ -95,6 +95,7 @@ builtinMixfix = Seq.fromList $ (HM.fromList <$>)
         builtinIdentifiers = identifier <$>
             [ "emptyset"
             , "naturals"
+            , "integers"
             , "rationals"
             , "reals"
             , "unit"
-- 
cgit v1.2.3


From 36e03142465e482f2b5506cd35dab5ef9cc9fd66 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 6 Jul 2024 19:53:50 +0200
Subject: Formalisation of rationals.

---
 library/numbers.tex      | 66 +++++++++++++++++++++++++-----------------------
 source/Syntax/Lexicon.hs |  1 +
 2 files changed, 35 insertions(+), 32 deletions(-)

(limited to 'source/Syntax')

diff --git a/library/numbers.tex b/library/numbers.tex
index 08cbc70..4ccba67 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -431,7 +431,14 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
 \end{axiom}
 
+\begin{axiom}\label{zero_less_one}
+    $\zero < 1$.
+\end{axiom}
 
+\begin{axiom}\label{reals_axiom_order_def}
+    Suppose $x,y,z,w \in \reals$.
+    If $x + y < z + w$ then $x < z \lor y < w$.
+\end{axiom}
 
 
 
@@ -501,42 +508,37 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 
 \subsection{The Rationals}
 
-%\begin{definition}
-%    $\inv{x} 
-%\end{definition}
-%
-%\begin{axiom}
-%    For all $x,y \in \reals$ we have $\rfrac{x}{y} \in \reals$.
-%\end{axiom}
-%
-%\begin{definition}
-%    $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \integers. q = \rfrac{z}{n} \}$.
-%\end{definition}
-
-
-
-
+\begin{axiom}\label{invers_reals}
+    For all $q \in \reals$ we have $\inv{q} \rmul q = 1$.
+\end{axiom}
 
+\begin{abbreviation}\label{rfrac}
+    $\rfrac{x}{y} = x \rmul \inv{y}$.
+\end{abbreviation}
 
+\begin{abbreviation}\label{naturalsplus}
+    $\naturalsPlus = \naturals \setminus \{\zero\}$.
+\end{abbreviation}
 
+\begin{definition}\label{rationals}
+    $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$.
+\end{definition}
 
 
-%\begin{signature}\label{invers_is_set}
-%    $\addInv{y}$ is a set.
-%\end{signature}
 
-%\begin{definition}\label{add_inverse}
-%    $\addInv{y} = \{ x \mid \exists k \in \reals. k + y = \zero \land x \in k\}$.
-%\end{definition}
-    
+\subsection{Order on the reals}
 
-%\begin{definition}\label{add_inverse_natural_language}
-%    $x$ is additiv inverse of $y$ iff $x = \addInv{y}$. 
-%\end{definition}
+\begin{lemma}\label{plus_one_order}
+    For all $r\in \reals$ we have $ r < r + 1$.
+\end{lemma}
+\begin{proof}
+    %Follows by \cref{reals_axiom_one,reals_axiom_order,reals_axiom_order_def,zero_less_one,reals}.
+\end{proof}
 
-%\begin{lemma}\label{rminus}
-%    $x \rminus \addInv{x} = \zero$.
-%\end{lemma}
+\begin{lemma}\label{negation_and_order}
+    Suppose $r \in \reals$.
+    $r \leq \zero$ iff $\zero \leq \neg{r}$.
+\end{lemma}
 
 
 
@@ -546,7 +548,7 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     Then $x + y$ is positiv.
 \end{lemma}
 \begin{proof}
-    Omitted.
+    
 \end{proof}
 
 \begin{lemma}\label{reals_mul_of_positiv}
@@ -688,6 +690,6 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 
 
 
-\begin{proposition}\label{safe}
-    Contradiction.
-\end{proposition}
+%\begin{proposition}\label{safe}
+%    Contradiction.
+%\end{proposition}
diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
index 65072ee..de6d966 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Syntax/Lexicon.hs
@@ -111,6 +111,7 @@ prefixOps =
     , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd"))
     , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow"))
     , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg"))
+    , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv"))
     , (ConsSymbol, (NonAssoc, "cons"))
     , (PairSymbol, (NonAssoc, "pair"))
     -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply"))
-- 
cgit v1.2.3


From c4894bc4e788fae079b76b824a8d86c167098cc8 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 12 Aug 2024 00:12:07 +0200
Subject: more more way more urysohn

---
 library/topology/urysohn.tex | 127 ++++++++++++++++++++++++++++++++++++++++---
 source/Api.hs                |   8 +--
 source/CommandLine.hs        |   5 +-
 source/Syntax/Lexicon.hs     |   1 +
 4 files changed, 127 insertions(+), 14 deletions(-)

(limited to 'source/Syntax')

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index f34f12f..6662706 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -36,7 +36,12 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-
+%%-----------------------
+%   Idea:
+%   A sequence could be define as a family of sets, 
+%   together with the existence of an indexing function.
+%
+%%-----------------------
 \begin{struct}\label{sequence}
     A sequence $X$ is a onesorted structure equipped with
     \begin{enumerate}
@@ -148,8 +153,9 @@ The first tept will be a formalisation of chain constructions.
 \end{definition}
 
 \begin{definition}\label{refinmant}
-    $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and 
-    for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$
+    $C'$ is a refinmant of $C$ iff $C'$ is a urysohnchain in $X$
+    and for all $x \in C$ we have $x \in C'$ 
+    and for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$
     and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$.
 \end{definition}
 
@@ -312,9 +318,9 @@ The first tept will be a formalisation of chain constructions.
     % U  = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n})
     % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ...   A_{n-1}, A'_{n}, A_{n})
 
-    Let $m = \max{\indexset[U]}$.
-    For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
-    such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$.
+    % Let $m = \max{\indexset[U]}$.
+    % For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
+    % such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$.
     
     
     %\begin{definition}\label{refinmant}
@@ -347,6 +353,58 @@ The first tept will be a formalisation of chain constructions.
 
 
 
+
+\begin{abbreviation}\label{sequence_of_functions}
+    $f$ is a sequence of functions iff $f$ is a sequence 
+    and for all $g \in \carrier[f]$ we have $g$ is a function.
+\end{abbreviation}
+
+\begin{abbreviation}\label{sequence_in_reals}
+    $s$ is a sequence of real numbers iff $s$ is a sequence 
+    and for all $r \in \carrier[s]$ we have $r \in \reals$.
+\end{abbreviation}
+
+
+
+\begin{axiom}\label{abs_behavior1}
+    If $x \geq \zero$ then $\abs{x} = x$.
+\end{axiom}
+
+\begin{axiom}\label{abs_behavior2}
+    If $x < \zero$ then $\abs{x} = \neg{x}$.
+\end{axiom}
+
+\begin{abbreviation}\label{converge}
+    $s$ converges iff $s$ is a sequence of real numbers 
+    and $\indexset[s]$ is infinite
+    and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
+    there exist $N \in \indexset[s]$ such that
+    for all $m \in \indexset[s]$ such that $m > N$ 
+    we have $\abs{\index[s](N) - \index[s](m)} < \epsilon$.
+\end{abbreviation}
+
+
+\begin{definition}\label{limit_of_sequence}
+    $x$ is the limit of $s$ iff $s$ is a sequence of real numbers
+    and $x \in \reals$ and 
+    for all $\epsilon \in \reals$ such that $\epsilon > \zero$
+    we have there exist $n \in \indexset[s]$ such that 
+    for all $m \in \indexset[s]$ such that $m > n$ 
+    we have $\abs{x - \index[s](n)} < \epsilon$.
+\end{definition}
+
+\begin{proposition}\label{existence_of_limit}
+    Let $s$ be a sequence of real numbers.
+    Then $s$ converges iff there exist $x \in \reals$ 
+    such that $x$ is the limit of $s$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -381,12 +439,65 @@ The first tept will be a formalisation of chain constructions.
 
     We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$.
     \begin{subproof}
-        Trivial.
+        Omitted.
     \end{subproof}
 
-    
+    For all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$.
 
 
+    %%------------- Maybe use Abstrect.hs line 368 "Local Function".
+
+    We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
+    and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ 
+    we have $f(x) = \rfrac{n}{\pot(m)}$.
+    \begin{subproof}
+        %   Fix $m \in \indexset[\zeta]$.
+        %   $\index[\zeta](m)$ is a urysohnchain in $X$.
+        %   
+        %   Follows by \cref{existence_of_staircase_function}.
+
+        Omitted.
+    \end{subproof}
+
+    
+
+    %The sequenc of the functions
+    Let $\gamma = \{
+        (n,f) \mid 
+        n \in \naturals \mid 
+        
+        \forall n' \in \indexset[\index[\zeta](n)].             
+        \forall x \in \carrier[X].      
+        
+
+        f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land
+
+
+        % (n,f) \in \gamma  <=>   \phi(n,f)
+        % with \phi (n,f) :=        (x \in (A_k) \ (A_k-1))                 =>      f(x) = ( k / 2^n )        
+        %                       \/  (x \notin A_k for all k \in {1,..,n}    =>      f(x) = 1 
+
+            (       (n' = \zero)   
+            \land   (x \in \index[\index[\zeta](n)](n')) 
+            \land   (f(x)= \zero) ) 
+        
+        \lor
+        
+            (       (n' > \zero)    
+            \land   (x \in \index[\index[\zeta](n)](n'))
+            \land   (x \notin \index[\index[\zeta](n)](n'-1))
+            \land   (f(x) = \rfrac{n'}{\pot(n)}) )
+            
+        \lor
+
+            (       (x \notin  \index[\index[\zeta](n)](n'))
+            \land   (f(x) = 1) )
+        
+    \}$.
+    
+    
+    
+     
 
     %Suppose $\eta$ is a urysohnchain in $X$.
     %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
diff --git a/source/Api.hs b/source/Api.hs
index f597153..3fb0ca2 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -292,10 +292,10 @@ exportMegalodon file = do
 -- | This could be expandend with the dump case, with dump off just this and if dump is on it could show the number off the task. For quick use
 showFailedTask :: (a, ProverAnswer) -> IO()
 showFailedTask (_, Yes ) = Text.putStrLn ""
-showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("Prover found countermodel: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
-showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("Contradictory axioms: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
-showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("Out of resources: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
-showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("Error at: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("\ESC[31mProver found countermodel: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("\ESC[31mContradictory axioms: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("\ESC[31mOut of resources: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("\ESC[31mError at: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
 --showFailedTask (_, _) = Text.putStrLn "Error!"
 
 
diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index 47efe22..711f7f0 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -87,15 +87,16 @@ run = do
                             Text.hPutStrLn stderr tptp
                         Error err tptp task -> do
                             putStr "Error at:"
+
                             Text.putStrLn task
                             Text.putStrLn err
                             Text.putStrLn tptp
                             
                 WithFailList -> liftIO case result of
-                    VerificationSuccess -> putStrLn "Verification successful."
+                    VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m"
                     VerificationFailure [] -> error "Empty verification fail"
                     VerificationFailure fails -> do
-                        putStrLn "Following task couldn't be solved by the ATP: "
+                        putStrLn "\ESC[35mFollowing task couldn't be solved by the ATP: \ESC[0m"
                         traverse_ showFailedTask fails
                         Text.hPutStrLn stderr "Don't give up!"
 
diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
index de6d966..4fe8730 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Syntax/Lexicon.hs
@@ -112,6 +112,7 @@ prefixOps =
     , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow"))
     , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg"))
     , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv"))
+    , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs"))    
     , (ConsSymbol, (NonAssoc, "cons"))
     , (PairSymbol, (NonAssoc, "pair"))
     -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply"))
-- 
cgit v1.2.3


From 32424a1efbd774e6beb06212dbaec6e55e92fcd5 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 24 Aug 2024 11:44:27 +0200
Subject: hlint suggestion

---
 source/Syntax/Adapt.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'source/Syntax')

diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index 3a8b3d6..622946a 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -27,7 +27,7 @@ scanChunk ltoks =
         matchOrErr re env pos = match re toks ?? error ("could not find lexical pattern in " <> env <> " at " <> sourcePosPretty pos)
     in case ltoks of
         Located{startPos = pos, unLocated = BeginEnv "definition"} : _ ->
-            matchOrErr definition "definition" (pos)
+            matchOrErr definition "definition" pos
         Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ ->
             matchOrErr abbreviation "abbreviation" pos
         Located{startPos = pos, unLocated = (BeginEnv "struct")} :_ ->
-- 
cgit v1.2.3


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

---
 library/wunschzettel.tex           |  9 +++++++++
 source/Api.hs                      |  4 +++-
 source/Syntax/Abstract.hs          |  7 +++++++
 source/Syntax/Adapt.hs             | 14 ++++++++++++++
 source/Syntax/Concrete.hs          | 27 ++++++++++++++++++++++++++-
 source/Syntax/Concrete/Keywords.hs | 10 ++++++++--
 6 files changed, 67 insertions(+), 4 deletions(-)

(limited to 'source/Syntax')

diff --git a/library/wunschzettel.tex b/library/wunschzettel.tex
index b2681fd..74ea899 100644
--- a/library/wunschzettel.tex
+++ b/library/wunschzettel.tex
@@ -45,6 +45,15 @@ Tupel struct
     % more proof but now i can use the function f
 
     % --------------------------------------------------------
+    \begin{equation}
+        X=
+        \begin{cases}
+          0, & \text{if}\ a=1 \\
+          1, & \text{otherwise}
+        \end{cases}
+      \end{equation}
+
+
 
 
 \end{proof}
diff --git a/source/Api.hs b/source/Api.hs
index 3fb0ca2..1bdf615 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -203,7 +203,9 @@ describeToken = \case
     EndEnv _ -> "end of environment"
     _ -> "delimiter"
 
-
+-- | gloss generates internal represantation of the LaTeX files.
+-- First the file will be parsed and therefore checkt for grammer.
+-- 'meaning' then transfer the raw parsed grammer to the internal semantics.
 gloss :: MonadIO io => FilePath -> io ([Internal.Block], Lexicon)
 gloss file = do
     (blocks, lexicon) <- parse file
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.
diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index 622946a..96fd76d 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -34,6 +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 signature "signature" pos
         _ -> []
 
 adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon
@@ -85,6 +87,18 @@ abbreviation = do
     skipUntilNextLexicalEnv
     pure [lexicalItem m]
 
+signatureIntro ::  RE Token [ScannedLexicalItem]  --since signiture is a used word of haskell we have to name it diffrentliy 
+signatureIntro = do
+    sym (BeginEnv "signature")
+    few notEndOfLexicalEnvToken
+    m <- label
+    few anySym
+    lexicalItem <- head
+    few anySym
+    sym (EndEnv "signature")
+    skipUntilNextLexicalEnv
+    pure [lexicalItem m]
+
 label :: RE Token Marker
 label = msym \case
     Label m -> Just (Marker m)
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index b51b738..51cc013 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -351,8 +351,23 @@ grammar lexicon@Lexicon{..} = mdo
 
     define           <- rule $ Define <$> (_let *> beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof
     defineFunction   <- rule $ DefineFunction <$> (_let *> beginMath *> varSymbol) <*> paren varSymbol <* _eq <*>  expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof
+    
 
-    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, qed]
+
+    -- Define $f $\fromTo{X}{Y} such that,         
+    -- Define function $f: X \to Y$,
+    -- \begin{align}
+    --      &x \mapsto 3*x      &,  
+    --      &x \mapsto 4*k+x    &, 
+    -- \end{align}
+    -- 
+    defineFunctionMathy <-  rule    $ DefineFunctionMathy 
+                                    <$> (_define *> beginMath *> varSymbol)           -- Define $ f
+                                    <*> _colon *> varSymbol <*> _to *> varSymbol      -- : 'var' \to 'var'
+                                    <*> localFunctionDefinitionAlign 
+
+
+    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed]
 
 
     blockAxiom  <- rule $ uncurry3 BlockAxiom     <$> envPos  "axiom" axiom
@@ -435,7 +450,17 @@ 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.
diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs
index 135cdac..b507e7e 100644
--- a/source/Syntax/Concrete/Keywords.hs
+++ b/source/Syntax/Concrete/Keywords.hs
@@ -108,7 +108,7 @@ _either = word "either" ? "either"
 _equipped :: Prod r Text (Located Token) SourcePos
 _equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with"
 _every :: Prod r Text (Located Token) SourcePos
-_every = (word "every") ? "every"
+_every = word "every" ? "every"
 _exist :: Prod r Text (Located Token) SourcePos
 _exist = word "there" <* word "exist" ? "there exist"
 _exists :: Prod r Text (Located Token) SourcePos
@@ -124,7 +124,7 @@ _for = word "for" ? "for"
 _forAll :: Prod r Text (Located Token) SourcePos
 _forAll = (word "for" <* word "all") <|> word "all" ? "all"
 _forEvery :: Prod r Text (Located Token) SourcePos
-_forEvery = (word "for" <* word "every") <|> (word "every") ? "for every"
+_forEvery = (word "for" <* word "every") <|> word "every" ? "for every"
 _have :: Prod r Text (Located Token) SourcePos
 _have = word "we" <* word "have" <* optional (word "that") ? "we have"
 _if :: Prod r Text (Located Token) SourcePos
@@ -220,3 +220,9 @@ _in :: Prod r Text (Located Token) SourcePos
 _in = symbol "∈" <|> command "in" ? "\\in"
 _subseteq :: Prod r Text (Located Token) SourcePos
 _subseteq = command "subseteq" ? "\\subseteq"
+_to :: Prod r Text (Located Token) SourcePos
+_to = command "to" ? "\\to"
+_mapsto :: Prod r Text (Located Token) SourcePos
+_mapsto = command "mapsto" ? "\\mapsto"
+_ampersand :: Prod r Text (Located Token) SourcePos
+_ampersand = symbol "&" ? "&"
\ No newline at end of file
-- 
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')

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 a253d06a0755c41dd321fc2e235c3332de63a8c7 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 26 Aug 2024 16:55:39 +0200
Subject: Non finished attemped to translate a local function defintion from
 abstract to internal

---
 source/Meaning.hs         | 15 +++++++++++++++
 source/Syntax/Internal.hs |  2 ++
 2 files changed, 17 insertions(+)

(limited to 'source/Syntax')

diff --git a/source/Meaning.hs b/source/Meaning.hs
index 834d8a6..30e13f8 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -605,9 +605,24 @@ glossProof = \case
         if domVar == argVar
             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
+        if funVar /= funVar2
+            then error "missmatched function names"
+            else Sem.DefineFunctionMathy funVar domVar ranVar argVar <*> glossLocalFunctionExprEach definitions <*> glossProof proof
     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
+    e <- glossExpr definingExpression
+    d <- glossFormula localDomain
+    pure (e,d)
+
+
 glossCase :: Raw.Case -> Gloss Sem.Case
 glossCase (Raw.Case caseOf proof) = Sem.Case <$> glossStmt caseOf <*> glossProof proof
 
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 44603ad..872ae06 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -436,6 +436,8 @@ data Proof
     | Define VarSymbol Term Proof
     | DefineFunction VarSymbol VarSymbol Term Term Proof
 
+    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol [(Term, Formula)] Proof
+
 deriving instance Show Proof
 deriving instance Eq   Proof
 deriving instance Ord  Proof
-- 
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')

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')

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 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

---
 library/topology/urysohn2.tex | 4 +++-
 source/Checking.hs            | 6 +++---
 source/Syntax/Concrete.hs     | 2 +-
 3 files changed, 7 insertions(+), 5 deletions(-)

(limited to 'source/Syntax')

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'
-- 
cgit v1.2.3


From 6acc5654f1702f2466006564a415546a3def16e3 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 27 Aug 2024 17:19:02 +0200
Subject: Feature Complete Finalised the proof output and goals. The Local
 Function definition now producces a Function f with the right domain and
 range, together with the rules presented in cases. Then proof goal of this
 local definition is set to for all x we have x is element of dom(f) if and
 only if x is in exactly one of the subdomains. This suffices as
 welldefindness check on f, besides the right range.

Further checks that should be implemented are the correct range of the function.
And optional subproof such that the presented goal can be check easily.
---
 library/topology/urysohn2.tex |  2 +-
 source/Checking.hs            | 37 ++++++++++++++++++++++++-------------
 source/Syntax/Internal.hs     | 10 ++++++++++
 3 files changed, 35 insertions(+), 14 deletions(-)

(limited to 'source/Syntax')

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index f2f6ef3..ea49a6c 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -46,7 +46,7 @@
 
     Define $f : X \to \reals$ such that  $f(x) = $
     \begin{cases}
-        &(x + x) &\text{if} x \in X
+        &(x + k) &\text{if} x \in X \land k \in \naturals
         & x &\text{if} x \neq \zero
         & \zero & \text{if} x = \zero
         % & x ,x \in X    <- will result in technicly ambigus parse
diff --git a/source/Checking.hs b/source/Checking.hs
index 7362c93..b43923c 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -555,30 +555,41 @@ checkProof = \case
             ,Asm (relationNoun (TermVar funVar))]
 
         goals <- gets checkingGoals
-        setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union
+        setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` localFunctionGoal definitions)]
         tellTasks
 
         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
+        assume (functionSubdomianExpression funVar argVar domVar (NonEmpty.toList definitions)) --behavior on the subdomians
         setGoals goals
         checkProof continue
 
+-- |Creats the Goal \forall x. x \in dom{f} \iff (phi_{1}(x) \xor (\phi_{2}(x) \xor (... \xor (\phi_{n}) ..)))
+--  where the phi_{i} are the subdomain statments
+localFunctionGoal :: NonEmpty (Term,Formula) -> Formula
+localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs
 
--- | Makes a conjunction of all the subdomain statments <- this has to be checked!!!! TODO!!!!!!
-subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula 
-subdomainConjuctionLocalFunction _ defintions = 
-    let stmts = [snd x | x <- NonEmpty.toList defintions]
-    in makeDisjunction stmts 
 
+-- We have our list of expr and forumlas, in this case normaly someone would write
+-- f(x) =  ....cases
+--      & (\frac{1}{k} \cdot x) &\text{if} x \in \[k, k+1\)
+--
+-- So therefore we have to check that all free varibels in lhs are free on rhs,
+-- since its an expression all varibals from the lhs has to be free on rhs. 
+--
+-- so we take (exp, frm) -> binding all free in exp 
+-- -> make forall [x, bound vars] x \in \dom(f) & frm => exp
 
-functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
-functionSubdomianExpression f a (x:xs) = singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a xs
-functionSubdomianExpression _ _ [] = []
 
-    
+functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
+functionSubdomianExpression f a d (x:xs) = singleFunctionSubdomianExpression f a d x : functionSubdomianExpression f a d xs
+functionSubdomianExpression _ _ _ [] = []
 
-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)))
+singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> (Term, Formula) -> Asm
+singleFunctionSubdomianExpression funVar argVar domVar (expr, frm) = let
+    boundVar = Set.toList (freeVars expr) in
+    let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr)
+    in Asm def
+    
 
 
 checkCalc :: Calc -> Checking
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 7046161..e83126d 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -324,6 +324,16 @@ makeDisjunction = \case
     [] -> Bottom
     es -> List.foldl1' Or es
 
+makeIff :: [ExprOf a] -> ExprOf a
+makeIff = \case
+    [] -> Bottom
+    es -> List.foldl1' Iff es
+    
+makeXor :: [ExprOf a] -> ExprOf a
+makeXor = \case
+    [] -> Bottom
+    es -> List.foldl1' Xor es
+
 finiteSet :: NonEmpty (ExprOf a) -> ExprOf a
 finiteSet = foldr cons EmptySet
     where
-- 
cgit v1.2.3


From 5362771c14eccd80fd1a3ab6521c3a6ad9bb7838 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 17 Sep 2024 00:36:24 +0200
Subject: Corrected Math Env Parsing

Since Latex has a really specify syntax for
\begin{cases} ... \end{cases}
The math mode in tokenizing had to be setup correctly.
---
 library/numbers.tex                         |  3 +++
 library/topology/real-topological-space.tex | 27 +++++++++++++++------------
 source/Syntax/Concrete.hs                   |  6 +++---
 source/Syntax/Token.hs                      |  8 ++++----
 4 files changed, 25 insertions(+), 19 deletions(-)

(limited to 'source/Syntax')

diff --git a/library/numbers.tex b/library/numbers.tex
index 406553e..ac0a683 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -613,6 +613,9 @@ Laws of the order on the reals
 
 \subsection{Order on the reals}
 
+\begin{axiom}\label{reals_order_is_transitive}
+    For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$.
+\end{axiom}
 
 
 \begin{lemma}\label{plus_one_order}
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index e5e17ef..d9790aa 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -70,7 +70,7 @@
     Then $\epsBall{x}{\epsilon}$ is inhabited.
 \end{lemma}
 \begin{proof}
-    $x < x + \epsilon$.
+    $x < x + \epsilon$ by \cref{reals_order_behavior_with_addition,realsplus,reals_axiom_zero_in_reals,reals_axiom_kommu,reals_axiom_zero}.
     $x - \epsilon < x$.
     $x \in \epsBall{x}{\epsilon}$.
 \end{proof}
@@ -104,12 +104,8 @@
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{reals_order_is_transitive}
-    For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$.
-\end{lemma}
-\begin{proof}
-    Omitted.
-\end{proof}
+
+
 
 \begin{lemma}\label{reals_order_plus_minus}
     Suppose $a,b \in \reals$.
@@ -207,12 +203,16 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
 \end{lemma}
 
+\begin{lemma}\label{one_in_realsplus}
+    $1 \in \realsplus$.
+\end{lemma}
+
 \begin{lemma}\label{reals_existence_addition_reverse}
     For all $\delta \in \reals$ there exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
 \end{lemma}
 \begin{proof}
     Fix $\delta \in \reals$.
-    Follows by \cref{reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}.
+    Follows by \cref{one_in_realsplus,reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}.
 \end{proof}
 
 \begin{lemma}\label{reals_addition_minus_behavior1}
@@ -260,7 +260,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     \end{subproof}
     We show that $\epsBall{x}{\epsilon} \subseteq \intervalopen{a}{b}$.
     \begin{subproof}
-        It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$.
+        It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$ by \cref{subseteq}.
         Fix $y \in \epsBall{x}{\epsilon}$.
     \end{subproof}
 
@@ -270,7 +270,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a,b,x,y \in \reals$.
     Suppose $a < b$.
     Suppose $x < y$.
-    If $a \leq x < y \leq b$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
+    Suppose $a \leq x < y \leq b$.
+    Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
 \end{lemma}
 \begin{proof}
     Omitted.
@@ -280,7 +281,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a,b,x,y \in \reals$.
     Suppose $a < b$.
     Suppose $x < y$.
-    If $a = x$ and $b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$.
+    Suppose $a = x$ and $b \leq y$.
+    Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$.
 \end{lemma}
 \begin{proof}
     Omitted.
@@ -290,7 +292,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a,b,x,y \in \reals$.
     Suppose $a < b$.
     Suppose $x < y$.
-    If $a \leq x$ and $b = y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
+    Suppose $a \leq x$ and $b = y$.
+    Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
 \end{lemma}
 \begin{proof}
     Omitted.
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 9d52995..7a89bea 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -373,15 +373,15 @@ grammar lexicon@Lexicon{..} = mdo
     --     3 & \text{else}     
     -- \end{cases}
 
-    functionDefineCase <- rule $ (,) <$> (_ampersand *> expr) <*> (_ampersand *> text _if *> formula)
+    functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula)
     defineFunctionMathy <-  rule    $ DefineFunctionMathy 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
                                     <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
                                     <*> (_to *> expr <* endMath <* _suchThat) 
                                     -- <*> (_suchThat  *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula))))
                                     -- <*> (_suchThat  *> align (many1 (varSymbol <* exprApp <*  formula)))
-                                    <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq <* endMath)
-                                    <*> cases (many1 functionDefineCase)
+                                    <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq )
+                                    <*> cases (many1 functionDefineCase) <* endMath <* optional _dot 
                                     <*> proof
 
 
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index 52da86a..53e1e6a 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -189,7 +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@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:))
                 Just t -> goNormal (f . (t:))
         goText f = do
             r <- optional textToken
@@ -205,7 +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 = 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:))
@@ -282,7 +282,7 @@ alignBegin = guardM isTextMode *> lexeme do
 casesBegin :: Lexer (Located Token)
 casesBegin = guardM isTextMode *> lexeme do
     Char.string "\\begin{cases}"
-    setMathMode
+    --setMathMode
     pure (BeginEnv "cases")
 
 -- | Parses a single end math token.
@@ -301,7 +301,7 @@ alignEnd = guardM isMathMode *> lexeme do
 casesEnd :: Lexer (Located Token)
 casesEnd = guardM isMathMode *> lexeme do
     Char.string "\\end{cases}"
-    setTextMode
+    --setTextMode
     pure (EndEnv "cases")
 
 
-- 
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')

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