diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-08-26 15:33:04 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-08-26 15:33:04 +0200 |
| commit | d79c85d70fc907858e3af5715bb94e8fdc202155 (patch) | |
| tree | dfe5abd1d17dd44fd58814071eff03a8b2e7c05b /source/Syntax/Abstract.hs | |
| parent | ce03d33eaa7e9d37935f225d48459223a4004a50 (diff) | |
I implemented a parsing rule in concrete.hs
for local functions and a abstract type in abstract.hs
for the proof data structure.
Diffstat (limited to 'source/Syntax/Abstract.hs')
| -rw-r--r-- | source/Syntax/Abstract.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index f775b69..6457d42 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -373,7 +373,7 @@ data Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol [VarSymbol Expr [VarSymbol] Expr ] Proof + | DefineFunctionMathy VarSymbol VarSymbol VarSymbol 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) |