In John Hughes's The Design of Pretty printing library paper, he says:
The implementations which we are trying to derive consist of equations of
a restricted form. We will derive implementations by proving their
constituent equations from the specification. By itself this is no
guarantee
Daryoush Mehrtash dmehrtash at gmail.com writes:
What does restricted form mean?
non-restricted: e.g., f (f x y) z = f x (f y z))
restricted: the shape of function declarations in Haskell
(where lhs is a pattern)
definitions are terminating ...
non-termination: an equation like f x y = f
