diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-16 02:12:06 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-16 02:12:06 +0200 |
| commit | 640fe16eaab00ea29046ef18e6f751571d923eaa (patch) | |
| tree | a15b2538f9895f54669251cd0ddf05c35ccf77d7 /library/topology/preclosure.tex | |
| parent | 3ef20da08eda23db76d763a2c6c7ee416348a021 (diff) | |
Missmatched Assume Error found. not fixed
In line 137 and 140 of real-topological-space.tex
Line 140 wont get parsed and line 140 will get parsed.
Case matching in Checking.hs is not working as intended.
Case phi@(Atomic p args) -> in line 960 in checking.hs
is not reached in checking of the Fixing with a symbol
Error Massage shows that < will be interpreted as a Term symbol there
not as a predicate.
Error Massage:
zf: MismatchedAssume (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "<"))) [TermVar (NamedVar "c"),TermVar (NamedVar "x")]) (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "rless"))) [TermVar (NamedVar "c"),TermVar (NamedVar "x")]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (NamedVar "c"),TermSymbol (SymbolMixfix [Just (Command "epsBall"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR,Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermVar (NamedVar "x"),TermVar (NamedVar "epsilon")]]))
Diffstat (limited to 'library/topology/preclosure.tex')
0 files changed, 0 insertions, 0 deletions