WIP: don't tie bi.weakestpre to program_logic.language (small canonical structure approach)
This is another attempt to fix #408 (closed), this time by adding a new canonical structure for just the val
and expr
types (so that we can define the Wp
notation based on that).
This seems to mostly work. I first tried to keep the val
and expr
fields in language
, but that does not work since then bi.weakestpre.expr LANG
(where LANG: language
) simplifies to program_logic.language.expr LANG
(reducing the coercion away), and subsequently canonical structure search fails.
So instead I embed pre_language
as a field into language
, which seems to work rather well -- except for one strange failure in proph_erasure
that I could not figure out.