felix.git/library/set.tex, branch hotgUnnamed repository; edit this file 'description' to name the repository.
https://git.adelon.net/felix.git/atom?h=hotg2026-08-03T21:28:44+00:00Stabilize one-core set proofs2026-08-03T21:28:44+00:00adelon22380201+adelon@users.noreply.github.com2026-08-03T21:28:44+00:00urn:sha1:cf1b39b5bd239da2bfd9e44321c9801424f89c4cAlign successor with canonical set insertion2026-08-02T20:02:39+00:00adelon22380201+adelon@users.noreply.github.com2026-08-02T20:02:39+00:00urn:sha1:e378c4000965613bf2399634ee76a7c25d73c980
Exact definitions remain named globals, so suc spells the canonical construction directly to coalesce with the packaged successor.
Separate ordered tuples from PairSet2026-08-02T18:51:00+00:00adelon22380201+adelon@users.noreply.github.com2026-08-02T18:51:00+00:00urn:sha1:63451bdca1f078eef1069cba9bba1b278fc31cdeRewrite protected set and naturals closure2026-08-02T16:42:54+00:00adelon22380201+adelon@users.noreply.github.com2026-08-02T16:42:54+00:00urn:sha1:5f64079c4ec671de04971f38907805e9de514537Track ownership of top-level symbols2026-07-03T00:13:21+00:00adelon22380201+adelon@users.noreply.github.com2026-07-03T00:13:21+00:00urn:sha1:40bc466d6a996e731cba21f24a58be08b1f22689
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.
Make handling of local variables stricter2026-04-12T13:25:03+00:00adelon22380201+adelon@users.noreply.github.com2026-04-12T13:25:03+00:00urn:sha1:bb4497227eb1ab060311baf0664865979655e03cAdd quantified calcs and relax tokenization2025-07-16T10:36:32+00:00adelon22380201+adelon@users.noreply.github.com2025-07-16T10:36:32+00:00urn:sha1:9aac1a22c4ff4b4be16800b86e34a94d358b0deb
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.
Linting and optimization2025-07-08T19:20:20+00:00adelon22380201+adelon@users.noreply.github.com2025-07-08T19:20:20+00:00urn:sha1:51fe28bdd9943e359de5835d2737c0fdc8618df7Basic proofs2025-07-07T14:00:15+00:00adelon22380201+adelon@users.noreply.github.com2025-07-07T14:00:15+00:00urn:sha1:5c9507fca014a81f9a694b31f3b2bdca71c2291cUpdate set.tex2025-07-07T13:53:29+00:00adelon22380201+adelon@users.noreply.github.com2025-07-07T13:53:29+00:00urn:sha1:0eb1252087134f860102a96f05a4de733063c769