Skip to content
GitLab

Generalize Propers for lists / Add some missing Params

Merged Robbert Krebbers requested to merge robbert/list_proper into master

For example, for fmap:

  • Old: Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f)
  • New: Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) fmap

This means that solve_proper can also find a Proper instance when the two functions are different, and then prove that they are extensionally equal.

This is similar to what we have done in !276 (merged) for maps.

Edited by Ralf Jung

Merge request reports