diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-08-27 01:44:45 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-08-27 01:44:45 +0200 |
| commit | 30f7c63ce566c993816607f3368c357233693aae (patch) | |
| tree | 9a4cae03dabe28aeda4d2f5537ee04a808b5c49f /source/Syntax/Abstract.hs | |
| parent | 76ea8e11d943b123d28dfbe2f354838f80fb8dba (diff) | |
Experimental working commit, programm will compile
But the Proof that the domain of the local function
is not right. Also if in the definition of our local
function we just use f(x) = x then we get a technical
ambigus parse
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 6372c87..13691e7 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -373,7 +373,7 @@ data Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof + | DefineFunctionMathy 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) |