summaryrefslogtreecommitdiff
path: root/source/Checking/Exact/Proof.hs
AgeCommit message (Collapse)Author
3 hoursMigrate to `Felix` namespaceHEADhotgadelon
27 hoursRetain formula-quantifier induction namesadelon
28 hoursRestore checked relational replacementadelon
28 hoursRetain source names for omitted set inductionadelon
29 hoursRestore checked set-induction compositionadelon
30 hoursConfine contradictory status to falsum targetsadelon
30 hoursRestore exact cases and contradictionadelon
31 hoursTighten exact calculation invariantsadelon
43 hoursRestore exact local reasoning proofsadelon
44 hoursCentralize checked set constructionsadelon
45 hoursComplete named construction premise viewsadelon
46 hoursRestore exact proof binder and witness formsadelon
2 daysUnify checked candidate planningadelon
2 daysPlan and admit module declarations prospectivelyadelon
2 daysRoute declarations through checked envelopesadelon
3 daysCompile exact structure declarationsadelon
4 daysSupport proof-local function graphsadelon
4 daysConfine indirect Vampire dischargeadelon
4 daysSupport terminal exact contradictionadelon
4 daysSupport proof-local set definitionsadelon
4 daysConfine set induction to outer proofsadelon
4 daysRewrite protected set and naturals closureadelon
4 daysNarrow final prelude validationadelon
4 daysRetain exact omitted-proof locationsadelon
4 daysConfine final prelude constructionadelon
4 daysConfine final prelude foundation leavesadelon
4 daysOpen exact claim envelopes in proofsadelon
5 daysLower exact omitted proofsadelon
5 daysDerive exact proof premise selectionadelon
5 daysConfine scoped proof compositionadelon
5 daysLocate exact proof obligation failuresadelon
5 daysCompile exact ordinary proofsadelon