summaryrefslogtreecommitdiff
path: root/source/Syntax
diff options
context:
space:
mode:
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