summaryrefslogtreecommitdiff
path: root/source
AgeCommit message (Expand)Author
3 hoursMigrate to `Felix` namespaceHEADhotgadelon
6 hoursMove to Felix namespaceadelon
6 hoursMove Version moduleadelon
6 hoursMore ZF droppingadelon
6 hoursRemove some ZF stuffadelon
7 hoursSimplify entry/CLI, track slowest ATP tasksadelon
22 hoursUpdate Core.hsadelon
23 hoursMake finite-set literals intrinsicadelon
24 hoursNormalize transparent inductive contextsadelon
25 hoursSupport exact nested inductive contextsadelon
26 hoursQualify definition migration diagnosticsadelon
26 hoursClose exact definition declaration boundaryadelon
26 hoursTighten quantified-term scope coverageadelon
27 hoursRestore quantified terms in proposition contextsadelon
27 hoursPin relational extensional schemaadelon
27 hoursRetain formula-quantifier induction namesadelon
28 hoursTest relational replacement transactionsadelon
28 hoursRestore checked relational replacementadelon
28 hoursRetain source names for omitted set inductionadelon
29 hoursTest general exact 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 hoursTest exact local reasoning admissionadelon
43 hoursRestore exact local reasoning proofsadelon
43 hoursSimplify checked set construction invariantsadelon
44 hoursAudit the exact Omega fact batchadelon
44 hoursCentralize checked set constructionsadelon
44 hoursRepair named separation regressionadelon
45 hoursComplete named construction premise viewsadelon
46 hoursRestore exact proof binder and witness formsadelon
47 hoursRestore implicit set construction routingadelon
48 hoursRestore fixed equality aliasesadelon
2 daysFix structure carrier membership loweringadelon
2 daysTighten executor and candidate invariantsadelon
2 daysBind Vampire completions to requestsadelon
2 daysUnify checked candidate planningadelon
2 daysMake Vampire resolution modes explicitadelon
2 daysCleanupadelon
2 daysUse two-worker Vampire portfolios by defaultadelon
2 daysName prospective lowering explicitlyadelon
2 daysValidate speculative admission orderingadelon
2 daysPlan and admit module declarations prospectivelyadelon
2 daysRoute declarations through checked envelopesadelon
2 daysSeparate declaration semantics from evidenceadelon
2 daysAdd owned Vampire request handlesadelon
3 daysName cleanupadelon
3 daysRemove Phase 0 migration residueadelon
3 daysPrioritize batch integrity failuresadelon