felix.git - Unnamed repository; edit this file 'description' to name the repository.

Age	Commit message (Collapse)	Author
4 hours	Migrate to `Felix` namespaceHEAD hotg	adelon

27 hours	Close exact definition declaration boundary	adelon

4 days	Separate ordered tuples from PairSet	adelon

10 days	Restore textual adjective signatures	adelon

10 days	Fix textual connective precedence	adelon

10 days	Parse transfinite induction continuation after method	adelon

11 days	Make `Omitted` carry its location	adelon

2026-07-23	Make `Contradiction` a proof-terminal keyword	adelon

2026-04-13	Implement datatypes	adelon

2026-03-07	Preserve marker for prefix predicates	adelon

2026-03-07	Add HTML rendering skeleton	adelon

2026-02-14	Simplify	adelon

2026-02-13	Collect more location information	adelon

2026-02-10	Fix checking of signatures	adelon

2026-02-06	Use tries for patterns, skip trivial hypotheses	adelon

2026-02-05	Remove `lookupLexicalItem`, attach info in AST instead	adelon

2026-02-05	Remove `lookupOp` and add marker to AST instead	adelon

2026-02-05	Prepare mixfix refactor	adelon

2026-02-05	Use `Map` over `HashMap`	adelon

2026-02-05	Optimize data structure used for translation	adelon
	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.
2025-12-17	Fix `filterTask`, make var names more consistent	adelon

2025-12-16	Add location info to implicit QED step	adelon

2025-12-14	Add more location info in tasks	adelon

2025-12-09	Propagate location info further	adelon

2025-12-09	Gather some location info from parser	adelon
	WIP
2025-11-27	Add basic parameter handling for relators	adelon

2025-08-12	Relax function symbol definitions	adelon
	Extra assumptions are simply discarded for now.
2025-08-12	Allow relation symbols with parameters	adelon
	Parameters must follow the relation symbol and be surrounded by braces, like so: `\rel{x}{y}{z}`. This attempt is still brittle/broken in a few ways: - It makes using braces in creative ways in mixfix notation ambiguous. - It does not verify that the parameters are used in a consistent manner for each symbol. It essentially allows users to define `a\MyRel b` and `a\MyRel{x} b` (and ones with even more parameters). - It allows parameters for all relation symbols, even for those where it makes no sense in ordinary TeX markup, e.g. `a <{x} b`.
2025-07-16	Add quantified calcs and relax tokenization	adelon
	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-18	working commit	Simon-Kor

2024-09-17	Corrected Math Env Parsing	Simon-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-27	ambigus parse fix. The proof goal must be changed,	Simon-Kor
	since now some could define a function with overlapping and worng subdomains
2024-08-27	Experimental working commit, programm will compile	Simon-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-08-26	Implemented the checking for local functions.	Simon-Kor

2024-08-26	I implemented a parsing rule in concrete.hs	Simon-Kor
	for local functions and a abstract type in abstract.hs for the proof data structure.
2024-08-24	First atemped to write a new way of local function defintion	Simon-Kor

2024-06-10	Dedupe helper function	adelon

2024-05-07	Sketch noun coord, symbols for reals	adelon

2024-02-10	Initial commit	adelon