summaryrefslogtreecommitdiff
path: root/source/Syntax
diff options
context:
space:
mode:
authorSimon-Kor <52245124+Simon-Kor@users.noreply.github.com>2024-08-26 16:55:39 +0200
committerSimon-Kor <52245124+Simon-Kor@users.noreply.github.com>2024-08-26 16:55:39 +0200
commita253d06a0755c41dd321fc2e235c3332de63a8c7 (patch)
tree495156e3c02735435e5a70ef5d2f70074b6598e1 /source/Syntax
parentd79c85d70fc907858e3af5715bb94e8fdc202155 (diff)
Non finished attemped to translate a local
function defintion from abstract to internal
Diffstat (limited to 'source/Syntax')
-rw-r--r--source/Syntax/Internal.hs2
1 files changed, 2 insertions, 0 deletions
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