Skip to content

State `bi_mono_pred` using `□`/`-∗` instead of `<pers>`/`→`.

Robbert Krebbers requested to merge robbert/bi_mono_pred into master

This follows the usual pattern of avoiding when possible.

The new statement should be logically equivalent, but easier to use.

Edited by Robbert Krebbers

Merge request reports