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_iff → decide_ext and bool_decide_iff → bool_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