Skip to content

Factor plainly out of main BI interface

Ralf Jung requested to merge ralf/plainly into gen_proofmode

The intention is to make the axioms compatible with plainly P r := forall s, P s in linear BIs. This is needed to obtain propositional extensionality.

Edited by Ralf Jung

Merge request reports