| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
Merge (finally)
|
|
Submission of Formalisation
|
|
|
|
|
|
in urysohn2.tex line 674 the secound 2 throws an ambiguous parse.
the same definition in line 678 commented without this a does not throe this error.
ambiguous parse: [BlockLemma (SourcePos {sourceName = "set.tex", sourceLine = Pos 129, sourceColumn = Pos 1}) (Marker "empty_eq") (Lemma [] (StmtConnected Implication (StmtVerbPhrase (TermExpr (ExprVar (NamedVar "x")) :| [TermExpr (ExprVar (NamedVar "y"))]) (VPAdj (Adj [Just (Word "empty")] [] :| []))) (StmtFormula (FormulaChain (ChainBase (ExprVar (NamedVar "x") :| []) Positive (RelationSymbol (Symbol "=")) (ExprVar (NamedVar "y") :| [])))))),BlockLemma (SourcePos {sourceName = "set.tex", sourceLine = Pos 129, sourceColumn = Pos 1}) (Marker "empty_eq") (Lemma [] (StmtConnected Implication (StmtConnected Conjunction (StmtVerbPhrase (TermExpr (ExprVar (NamedVar "x")) :| []) (VPVerb (Verb (SgPl {sg = [], pl = []}) []))) (StmtVerbPhrase (TermExpr (ExprVar (NamedVar "y")) :| []) (VPAdj (Adj [Just (Word "empty")] [] :| [])))) (StmtFormula (FormulaChain (ChainBase (ExprVar (NamedVar "x") :| []) Positive (RelationSymbol (Symbol "=")) (ExprVar (NamedVar "y") :| []))))))]
|
|
|
|
|
|
Since Latex has a really specify syntax for
\begin{cases} ... \end{cases}
The math mode in tokenizing had to be setup correctly.
|
|
|
|
|
|
|
|
|
|
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")]]))
|
|
At line 137 in real-topological-space.tex
Can't use Fix at this point.
|
|
In Line 49 in real-topological-space.tex the Fix can't be processed.
|
|
Error:
zf: Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: TermSep (NamedVar "n") (TermSymbol (SymbolMixfix [Just (Command "naturals")]) []) (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "rless"))) [TermSymbol (SymbolInteger 1) [],TermVar (B ())]))
CallStack (from HasCallStack):
error, called at source/Encoding.hs:89:13 in zf-0.3.0.0-3mIpbM9y9fK3yXjxxoLDb2:Encoding
|
|
|
|
|
|
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")]]))
|
|
|
|
|
|
Merge branch 'feature_function_definitions' into formalisation_numbers
|
|
Hot Fix for the wrong Asumtion creation. Now the function will have a image.
|
|
|
|
|
|
Contradiction was due to a misstake in the definition in sequence.
|
|
False can be proven with
iff_sequence, codom_of_emptyset_can_be_anything,sequence,
emptyset_is_function_on_emptyset,id_dom,in_irrefl,
suc_subseteq_implies_in,emptyset_subseteq
|
|
|
|
|
|
|
|
|
|
|
|
Finalised the proof output and goals.
The Local Function definition now producces a Function f with the right
domain and range, together with the rules presented in cases.
Then proof goal of this local definition is set to
for all x we have x is element of dom(f) if and only if x is in exactly one of the subdomains.
This suffices as welldefindness check on f, besides the right range.
Further checks that should be implemented are the correct range of the function.
And optional subproof such that the presented goal can be check easily.
|
|
since now some could define a function with overlapping
and worng subdomains
|
|
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
|
|
|
|
function defintion from abstract to internal
|
|
for local functions and a abstract type in abstract.hs
for the proof data structure.
|
|
|
|
|
|
|
|
|
|
|
|
resloved some proofing complications, but
they can prove flase together with lemmas about
ordinal, the exat lemma are in urysohn.tex at
line 522.
|
|
|
|
|
