Skip to content

Remove plainly_exist_1 from the BI axioms.

Jacques-Henri Jourdan requested to merge jh/exist_plainly into gen_proofmode

Added a PlainlyExist1BI class for BIs that do have the property.

One slight annoyance is that this class has to appear in interface.v. Otherwise, we have to add a dependency uPred.v -> bi/derived.v, which kill parallelism. Just tell me if you prefer this over the current alternative.

Edited by Robbert Krebbers

Merge request reports