[Haskell-cafe] What does it mean to derive "equations of restricted from" in Haskell?
dmehrtash at gmail.com
Tue Jul 16 10:19:01 CEST 2013
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 that the implemented functions satisfy the specification because
> we might not have proved enough equation But if we also check that the
> derived definitions are terminating and exhaustive then this property is
What does "restricted form" mean?
What is the meaning and significance of "definitions are terminating and
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe