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

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

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

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