Skip to content
GitLab

Draft: move bi_persistently_emp out of BI interface, and get a basic proof mode working again

Open Ralf Jung requested to merge ralf/bi-persistently-emp into master

This makes the proofmode work with an arbitrary BI, even ones that do not have a sensible persistence modality: one can pick const False as the modality to satisfy all the remaining mandatory laws.

Based on !881 (merged) Fixes #425

Edited by Ralf Jung