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 > guaranteed" What does "restricted form" mean? What is the meaning and significance of "definitions are terminating and exhaustive"? -- Daryoush Weblog: http://onfp.blogspot.com/
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
