diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-08-27 02:13:29 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-08-27 02:13:29 +0200 |
| commit | 604d7a87b4c45ab13ef03e3c7a611ad4f9342f23 (patch) | |
| tree | f5121f17d97dba1df8a815b0b21abfeb01c50513 /source/Checking.hs | |
| parent | 30f7c63ce566c993816607f3368c357233693aae (diff) | |
ambigus parse fix. The proof goal must be changed,
since now some could define a function with overlapping
and worng subdomains
Diffstat (limited to 'source/Checking.hs')
| -rw-r--r-- | source/Checking.hs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/source/Checking.hs b/source/Checking.hs index 6d55ee1..7362c93 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -564,11 +564,11 @@ checkProof = \case checkProof continue --- | Makes a conjunction of all the subdomain statments +-- | Makes a conjunction of all the subdomain statments <- this has to be checked!!!! TODO!!!!!! subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula -subdomainConjuctionLocalFunction argVar defintions = +subdomainConjuctionLocalFunction _ defintions = let stmts = [snd x | x <- NonEmpty.toList defintions] - in TermVar argVar `IsElementOf` makeConjunction stmts + in makeDisjunction stmts functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm] |