diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-04 15:17:50 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-04 15:17:50 +0200 |
| commit | 68716d1ab46dee3dfc1b03089f941dbb6883cdcd (patch) | |
| tree | 7539b439e1407b8ec02a97006adfd039b12c9ccf /source/Checking.hs | |
| parent | c57360cf062805c86fed5d1f3f4adbf52c05f9ff (diff) | |
Mismatched Assume in Induction
Unexpeced Mismatch in line 99 and 109 or the pair
100 and 108. Parsing works with line 99 and 108 or with
the lines 100 and 109.
zf: MismatchedAssume (TermSymbol (SymbolPredicate (PredicateNoun (SgPl {sg = [Just (Word "natural"),Just (Word "number")], pl = [Just (Word "natural"),Just (Word "numbers")]}))) [TermVar (NamedVar "n")]) (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (NamedVar "n"),TermSymbol (SymbolMixfix [Just (Command "naturals")]) []]) (TermSymbol (SymbolPredicate (PredicateVerb (SgPl {sg = [Just (Word "has"),Just (Word "cardinality"),Nothing], pl = [Just (Word "ha"),Just (Word "cardinality"),Nothing]}))) [TermSymbol (SymbolMixfix [Just (Command "seq"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR,Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermSymbol (SymbolMixfix [Just (Command "emptyset")]) [],TermVar (NamedVar "n")],TermSymbol (SymbolMixfix [Just (Command "suc"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermVar (NamedVar "n")]]))
Diffstat (limited to 'source/Checking.hs')
0 files changed, 0 insertions, 0 deletions