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

Age	Commit message (Collapse)	Author
3 days	Remove obsolete verification machinery	adelon

4 days	Locate invalid datatype premises	adelon

4 days	Lower fixed exact set terms uniformly	adelon

5 days	Prepare exact inductive declarations	adelon

6 days	Render checking markers directly	adelon

6 days	Restore precise verification diagnostics	adelon

6 days	Require stores for verification commands	adelon

9 days	Bind typed fact admission to module builders	adelon

9 days	Check direct inductives through fixed-point replay	adelon

9 days	Authorize atomic facts through exact typed imports	adelon

9 days	Authorize ground reflexivity through kernel replay	adelon
	The first typed fact family is deliberately dependency-free. Its rows remain outside the legacy fact registry, so unmigrated declarations cannot consume or reauthorize them.
9 days	Assign nominal identities to predicate signatures	adelon

9 days	Check admitted modules sequentially	adelon

9 days	Authorize legacy declaration batches	adelon

9 days	Prepare complete legacy obligation batches	adelon

10 days	Reject unresolved structure operations before encoding	adelon

10 days	Return typed errors for malformed proof shapes	adelon

10 days	Make dependency paths nonempty	adelon

10 days	Make inductive declarations transactional	adelon

10 days	Make ordinary facts transactional	adelon

10 days	Make signatures transactional	adelon

10 days	Make abbreviations and definitions transactional	adelon

10 days	Validate canonical datatype recursion	adelon

10 days	Allocate task-local TPTP names	adelon
	Distinct target variable names exposed a replacement-condition scope lift that source-derived names had masked. Keep those variables under the replacement existential.
10 days	Make structure registration transactional	adelon

10 days	Remove source annotations from TPTP tasks	adelon

10 days	Reject unsound disjunctive `Assume` reduction	adelon

11 days	Make `Omitted` carry its location	adelon

14 days	Prevent self-referential definitions	adelon

14 days	Reject Object-Symbol Marker Collisions	adelon

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

2026-07-23	Use semantic subset formula inside inductive defns	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	Reserve internal labels generated by datatypes	adelon

2026-04-13	Implement datatypes	adelon

2026-04-12	Refine handling of struct labels	adelon

2026-04-12	Make handling of local variables stricter	adelon

2026-02-24	Use shorter `_local_N` marker in TPTP output	adelon

2026-02-22	Add `INVARIANT` note to `checkingGoals`	adelon

2026-02-22	Fail earlier for nested comprehensions	adelon

2026-02-22	Fix proof-local definitions with replacement	adelon

2026-02-14	Fix induction rule validation	adelon

2026-02-13	Stream parsing and glossing	adelon

2026-02-13	Stop passing on lexicon	adelon

2026-02-13	Use callbacks instead of Writer	adelon

2026-02-10	Fix checking of signatures	adelon

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

2026-02-05	Cache hypothesis line	adelon

2026-02-05	Cache encoding of hypotheses	adelon

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