Skip to content

Add instance for `FromSep (tc_opaque P) Q1 Q2`

Robbert Krebbersrequested to merge
robbert/from_sep_opaque_fix into master

See discussion at !833 (diffs, comment 83516)

  • Turns out the cost/comment for FromAnd is obsolete, FromAnd is never used by iCombine
  • I removed the Hint Mode for FromAnd that corresponds to it being used by iCombine
  • Turns out there was an instance for missing for tc_opaque + FromSep
  • I added that instance with the correct cost + a better comment + a test case that used to fail prior to this MR

Merge request reports