diff options
Diffstat (limited to 'source/Syntax/Abstract.hs')
| -rw-r--r-- | source/Syntax/Abstract.hs | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 4aa8623..c8022c7 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -369,6 +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. |