felix.git/test/examples, branch hotg Unnamed repository; edit this file 'description' to name the repository. https://git.adelon.net/felix.git/atom?h=hotg 2026-08-05T20:18:50+00:00 Make finite-set literals intrinsic 2026-08-05T20:18:50+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-05T20:18:50+00:00 urn:sha1:84041116c7e9d8a3f5e6336c6d36dc39a8759ed6 Migrate historical parity examples 2026-08-05T19:16:47+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-05T19:16:47+00:00 urn:sha1:7e45956e151910831fbe35340ef1cb0d40614218 Build module-local syntax interfaces 2026-07-30T21:13:36+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-30T21:13:36+00:00 urn:sha1:0f0b966d958464f08b6efa39f9eee38d96509c19 Check direct inductives through fixed-point replay 2026-07-28T12:54:42+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T12:54:42+00:00 urn:sha1:ba4acdaa305d01469f66cd316edde4d22ea2fff9 Validate relation parameter arity 2026-07-27T16:19:29+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-27T15:32:47+00:00 urn:sha1:3b573d94d4c5e82802745daa7c7d679727155e7d Use semantic subset formula inside inductive defns 2026-07-23T17:56:52+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-23T17:56:52+00:00 urn:sha1:d1d3f178db000a6ffd928a75af8eb1ba2b7f8b9a Track ownership of top-level symbols 2026-07-03T00:13:21+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-03T00:13:21+00:00 urn: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. Implement datatypes 2026-04-13T20:50:05+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-04-13T20:50:05+00:00 urn:sha1:308afa734be012233673821deeeb9d440cc82dcb Handle bounded calculations 2026-04-12T20:03:56+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-04-12T20:03:56+00:00 urn:sha1:78379138430db3ae0575be8148b2646e8685f834 Update tests 2025-11-27T21:50:49+00:00 adelon 22380201+adelon@users.noreply.github.com 2025-11-27T21:50:49+00:00 urn:sha1:d1043cccea094fc3a0c37fbd84c0eead434890e5