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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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