summaryrefslogtreecommitdiff
path: root/source/Syntax/Token.hs
AgeCommit message (Collapse)Author
3 hoursMigrate to `Felix` namespaceHEADhotgadelon
2 daysCleanupadelon
3 daysIgnore commented source environmentsadelon
7 daysAccept empty source modulesadelon
10 daysMake parsed syntax deeply evaluableadelon
10 daysValidate packed source positions during lexingadelon
10 daysLoad selected sources as strict UTF-8adelon
2026-04-12Make lexer more robustadelon
2026-03-07Improve variable renderingadelon
2026-02-17Allow ticks in subscript of varsadelon
This also changes the encoding of the ticks in TPTP to just an underscore.
2026-02-13Use packed representation for `Location`adelon
2025-12-09Propagate location info furtheradelon
2025-12-03Fix skipping of starting charsadelon
2025-11-30Fix skipping to imports, drop charset depadelon
2025-11-29Integrate chunker and import gatherer into lexeradelon
Drops dependency on `regex-applicative-text`.
2025-08-23Update Token.hsadelon
2025-07-16Relax label syntaxadelon
2025-07-16Add quantified calcs and relax tokenizationadelon
Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems.
2024-09-17Corrected Math Env ParsingSimon-Kor
Since Latex has a really specify syntax for \begin{cases} ... \end{cases} The math mode in tokenizing had to be setup correctly.
2024-08-27Experimental working commit, programm will compileSimon-Kor
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
2024-05-22Allow `\left` and `\right` everywhereadelon
2024-05-21Allow line breaks via `\textbox`, handle `\left`/`\right`adelon
2024-05-16Attach whitespace info to located tokenadelon
2024-04-01Allow numbers in markers (from the second char)adelon
2024-03-28Allow Windows-style newlinesSimon-Kor
2024-02-10Initial commitadelon