Skip to content

don't tie bi.weakestpre to program_logic.language (full TC approach)

Ralf Jung requested to merge ralf/tc-weakestpre into master

This is my first attempt to fix #408 (closed), by making expr and val separate typeclass parameters of Wp. That fails type-checking in cases where coercions are involved, since TC inference fails before coercions are inserted (so e.g. using a val as the expression of the WP fails). We only rarely rely on this (3 times total in Iris master, and all of them in tests/), but it would be a breaking change.

Edited by Ralf Jung

Merge request reports