felix.git/source/Checking/Kernel/Semantics.hs, branch hotg Unnamed repository; edit this file 'description' to name the repository. https://git.adelon.net/felix.git/atom?h=hotg 2026-08-06T15:54:00+00:00 Migrate to `Felix` namespace 2026-08-06T15:54:00+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-06T15:54:00+00:00 urn:sha1:82328890108bae64b372b8d58620ebc62699de76 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