search

plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.36k stars 307 forks source link

Generalize and move postulation of `foldr-++` #998

Closed adql closed 4 months ago

adql commented 4 months ago

Generalize the operator to A → B → B like in foldr, so that the solution is usable in exercise foldr-∷ that follows. Also move the postulation to the appropriate location in the exercise itself.

Closes #997.