summaryrefslogtreecommitdiff
path: root/source/Checking.hs
diff options
context:
space:
mode:
authorSimon-Kor <52245124+Simon-Kor@users.noreply.github.com>2024-09-18 00:01:42 +0200
committerSimon-Kor <52245124+Simon-Kor@users.noreply.github.com>2024-09-18 00:01:42 +0200
commitc943ca6441e9118bc9caee1c11f697da89bc06b7 (patch)
tree1bfff18c501b0b8fa28d54848168d6b9ea06f12c /source/Checking.hs
parenta9785eb4cac6b8c237173f7e14367babd79e92e1 (diff)
working commit
Diffstat (limited to 'source/Checking.hs')
-rw-r--r--source/Checking.hs2
1 files changed, 1 insertions, 1 deletions
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)