Skip to content

Internal fractional tweaks.

Robbert Krebbers requested to merge robbert/internal_fractional_tweaks into master
  • Add Params instance and Proper instances.
  • Use tc_opaque to prevent iFrame/iNext from unfolding. (Since the definition is universally quantified, I think it's difficult to make a test this does not happen; unless it exposes the TC search debug info.)
  • Use ∗-∗ in iff lemma to remove BiAffine.

Merge request reports