summaryrefslogtreecommitdiff
path: root/source/Checking/Kernel/Derivation.hs
AgeCommit message (Expand)Author
4 hoursMigrate to `Felix` namespaceHEADhotgadelon
5 daysPrepare exact inductive declarationsadelon
9 daysFall back after reconstruction exhaustionadelon
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
9 daysAuthorize ground reflexivity through kernel replayadelon
9 daysReplay equality reflexivity independentlyadelon