summaryrefslogtreecommitdiff
path: root/source/Syntax/Abstract.hs
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2025-07-04 02:03:41 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2025-07-04 02:03:41 +0200
commitce19e88e04393cbed1f893a428cfa7369ccd0338 (patch)
tree87d545dbf600a08c1f04aa49b8531787c6c7040d /source/Syntax/Abstract.hs
parentec53cb7ff7cd6cbcaae578bdd430f48903ae789d (diff)
Fix whitespace
Diffstat (limited to 'source/Syntax/Abstract.hs')
-rw-r--r--source/Syntax/Abstract.hs10
1 files changed, 5 insertions, 5 deletions
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index c8022c7..c8d5dac 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -369,13 +369,13 @@ data Proof
-- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/.
-- The first 'VarSymbol' is the newly defined symbol, the second one is the argument.
-- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function).
-
-
-
-
+
+
+
+
| DefineFunctionLocal VarSymbol VarSymbol Expr 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)
-- | An inline justification.