Skip to content

Homomorphism properties for `bool_decide` + rename (bool_)decide_iff.

Robbert Krebbers requested to merge robbert/bool_decide into master
  • Add homomorphism properties for bool_decide and True, False, →,
  • Rename decide_iffdecide_ext and bool_decide_iffbool_decide_ext because _iff is now used for the above property for . This is also more consistent with other extensionality properties.
Edited by Robbert Krebbers

Merge request reports