summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2026-02-05Prepare mixfix refactoradelon
2026-02-05Skip TPTP ASTadelon
2026-02-05Use `Map` over `HashMap`adelon
2026-02-05Optimize data structure used for translationadelon
Splits mixfix data in lexicon into two data structures: a precedence table used for the parser and a mapping from symbols to markers used for the TPTP export.
2026-02-04Update Lexicon.hsadelon
2026-02-04Update Api.hsadelon
2026-01-31Compute parser only onceadelon
2026-01-30Link dump behaviour to cachingadelon
Run with `--uncached` if you want to dump all tasks.
2026-01-23Add directness annotation to TPTP outputadelon
2026-01-20Fix `syntacticMatch` issue with complex termsadelon
2026-01-13Add gloss of `AsmLetEq`adelon
2026-01-13Improve glossing errorsadelon
2026-01-09Improve errors for `fix` steps and unknown markersadelon
2026-01-07Fix error message for duplicate markersadelon
2026-01-06Use `equivalent` for term comparisonadelon
2026-01-06Quick work-around for term equality in assumptionadelon
2025-12-17Fix `filterTask`, make var names more consistentadelon
2025-12-16Add location info to implicit QED stepadelon
2025-12-14Fix column locationadelon
2025-12-14Add more location info in tasksadelon
2025-12-14Add location info to conjectureadelon
Still some `<nowhere>` value as placeholder left over.
2025-12-13More explicit `locate` for `Stmt`adelon
Fixes missing match on the `Just` case for `StmtConnected`
2025-12-13Start inlining more testsadelon
2025-12-12Update `ReplExpr` definitionsadelon
2025-12-11Optimize proof step for Vampire 5.0.0adelon
2025-12-11More on indexed variablesadelon
2025-12-10Propagate Location to CheckingErroradelon
2025-12-09Propagate location info furtheradelon
2025-12-09Gather some location info from parseradelon
WIP
2025-12-08Pass through markers with `throwWithMarker`adelon
2025-12-04Sketch out exprs with scoped de Bruijn indicesadelon
2025-12-04Remove Iota from internal syntaxadelon
2025-12-03Bump tested Vampire version to 5.0.0adelon
2025-12-03Fix skipping of starting charsadelon
2025-12-03Update tutorial.mdadelon
2025-12-03Update regularity.texadelon
2025-12-02Update tutorial.mdadelon
2025-12-02Update tutorial.mdadelon
2025-12-02Update tutorial.mdadelon
2025-12-02Update tutorial.mdadelon
2025-12-02Create tutorial.mdadelon
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-11-28Update for newer text-builderadelon
2025-11-27Update testsadelon
2025-11-27Add basic parameter handling for relatorsadelon
2025-11-27Update errors and cull formalizationsadelon
2025-08-23Update Token.hsadelon
2025-08-23Update urysohntwo.texadelon
2025-08-14Improve scanningadelon
Fixes scanning of relation symbols and adds a few error cases for function symbols.
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 22:19:55 +0000