summaryrefslogtreecommitdiff
path: root/source/Checking/Typed/Inductive.hs
AgeCommit message (Collapse)Author
4 hoursMigrate to `Felix` namespaceHEADhotgadelon
25 hoursNormalize transparent inductive contextsadelon
26 hoursSupport exact nested inductive contextsadelon
2 daysRestore fixed equality aliasesadelon
4 daysLower fixed exact set terms uniformlyadelon
4 daysPrepare exact datatype declarationsadelon
5 daysAuthorize exact guarded rule setsadelon
5 daysPrepare exact inductive declarationsadelon
5 daysLower exact finite-set notationadelon
9 daysSimplify typed inductive fact preparationadelon
9 daysPrepare direct inductive kernel proofsadelon