Skip to content

sum_list / max_list <-> foldr

Sanjit Bhatrequested to merge
sanjit/stdpp:sum-list-foldr into master

in this PR, I:

  • prove that sum_list and max_list correspond to foldr.
  • this lets me easily prove a Proper instance for Permutation.
  • using this, i simplify the proof that reverse is preserved by the two ops.

this resolves most of #111 (closed), except for adding TC opaqueness. is this necessary? i'd imagine that since the correspondence is only an equality lemma, it won't get used in TC search.

Merge request reports