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

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

23 hours	Make finite-set literals intrinsic	adelon

3 days	Remove the residual legacy task model	adelon

4 days	Locate invalid datatype premises	adelon

10 days	Validate relation parameter arity	adelon

10 days	Make structure registration transactional	adelon

10 days	Remove source annotations from TPTP tasks	adelon

11 days	Make `Omitted` carry its location	adelon

14 days	Reject Object-Symbol Marker Collisions	adelon

14 days	Make `Contradiction` a proof-terminal keyword	adelon

2026-07-03	Track ownership of top-level symbols	adelon
	Require every ownable top-level symbol to be introduced by a dedicated owner before it can appear in facts. Reject duplicate ownership and prevent symbols used by inductive definitions from being defined later. Use the ownership/dependency information to reject hidden recursive inductive definitions and to generate referenceable inductive principles. BREAKING CHANGE: Top-level facts no longer introduce symbols implicitly.
2026-04-13	Implement datatypes	adelon

2026-04-12	Refine handling of struct labels	adelon

2026-02-13	Collect more location information	adelon

2026-02-10	Fix checking of signatures	adelon

2026-02-05	Clean imports	adelon

2026-02-05	Cache hypothesis line	adelon

2026-02-05	Cache contraction	adelon

2026-02-05	Cache encoding of 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-01-20	Fix `syntacticMatch` issue with complex terms	adelon

2026-01-06	Use `equivalent` for term comparison	adelon

2026-01-06	Quick work-around for term equality in assumption	adelon

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 location info to conjecture	adelon
	Still some `<nowhere>` value as placeholder left over.
2025-12-09	Propagate location info further	adelon

2025-12-09	Gather some location info from parser	adelon
	WIP
2025-12-04	Remove Iota from internal syntax	adelon

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.
2025-07-02	Add TODO	adelon

2024-09-18	working commit	Simon-Kor

2024-08-27	Feature Complete	Simon-Kor
	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.
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	Non finished attemped to translate a local	Simon-Kor
	function defintion from abstract to internal
2024-02-10	Initial commit	adelon