summaryrefslogtreecommitdiff
path: root/source/Test/Unit/Kernel.hs
AgeCommit message (Collapse)Author
3 hoursMigrate to `Felix` namespaceHEADhotgadelon
25 hoursSupport exact nested inductive contextsadelon
3 daysRemove obsolete verification machineryadelon
5 daysPrepare exact inductive declarationsadelon
9 daysRemove obsolete kernel authorization projectionadelon
9 daysPrepare direct inductive kernel proofsadelon
9 daysDefine bounded fixed-point kernel rulesadelon
9 daysReplay scoped HOL derivations independentlyadelon
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.
9 daysReplay equality reflexivity independentlyadelon