felix.git/source/Syntax/Internal.hs, branch hotg Unnamed repository; edit this file 'description' to name the repository. https://git.adelon.net/felix.git/atom?h=hotg 2026-08-03T19:43:27+00:00 Remove the residual legacy task model 2026-08-03T19:43:27+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-03T19:43:27+00:00 urn:sha1:0ee278cf2894e7380ddafc273241ff2184ca7140 Locate invalid datatype premises 2026-08-02T09:49:59+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-02T09:34:54+00:00 urn:sha1:1a5a90ac0c8a88f4076cc77c82159609f92080e4 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 Make structure registration transactional 2026-07-27T16:19:29+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-27T14:23:12+00:00 urn:sha1:4a65f1430fdf3e8d75c36b5d74e07deb07b17f9e Remove source annotations from TPTP tasks 2026-07-27T16:19:29+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-27T02:42:09+00:00 urn:sha1:904ca07b7a89e3a91420876ef08e7113aae906e4 Make `Omitted` carry its location 2026-07-26T10:42:27+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-26T10:42:27+00:00 urn:sha1:108b963ebe395ec7c75234e5069c31732531fc97 Reject Object-Symbol Marker Collisions 2026-07-23T22:01:14+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-23T22:01:14+00:00 urn:sha1:ebdcfd251236b64774ce6c57009f4543d63647e5 Make `Contradiction` a proof-terminal keyword 2026-07-23T19:19:47+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-23T19:19:47+00:00 urn:sha1:f273a3fd299796a5f2e5b1ec83f2d87621b4ae73 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