felix.git/source/Test/Unit/Kernel.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:00:28+00:00 Remove obsolete verification machinery 2026-08-03T19:00:28+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-03T19:00:28+00:00 urn:sha1:5cdde1fd0f976863ae4b5831ab389048138b06a4 Prepare exact inductive declarations 2026-08-02T00:33:14+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-02T00:33:14+00:00 urn:sha1:d55d2416bc4f6a9aa055a17deae4fba0fe906316 Remove obsolete kernel authorization projection 2026-07-28T19:05:10+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T18:18:16+00:00 urn:sha1:a03cd6977c4eecbb590f4c9df01bbe0569c37a42 Prepare direct inductive kernel proofs 2026-07-28T12:51:24+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T12:47:19+00:00 urn:sha1:331d86e4a00bae144b6539edeb1deb9af78c5c7e Define bounded fixed-point kernel rules 2026-07-28T11:04:12+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T11:04:12+00:00 urn:sha1:63503003ca8022ad9890396866f52bf56bcb252d Replay scoped HOL derivations independently 2026-07-28T10:25:32+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T10:25:32+00:00 urn:sha1:ed12d0e4bcafd87e73219915ff8a3ae563c4a4cb Replay rechecks stored terms against the current global signature and bounds nodes, lexical depth, and conversion. Import-bearing trees remain replay-only until exact transition-inventory authorization alignment lands. Replay equality reflexivity independently 2026-07-28T09:39:11+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T09:39:11+00:00 urn:sha1:4076fc7c63032c0b698a3be9f46a7d14616dae5e