previous up next
Go backward to Hidden Data Structures
Go up to Top
Go forward to Combining Universal and Existential Quantification
RISC-Linz logo

Hidden Data Types

package point2
   type Point is private;
   function makepoint(x: Real, y: Real) return Point;
   - - hidden local definition of type Point
end point2;

type Point2 =
   exists Point.
      {makepoint: (Real x Real) -> Point,
type Point2WRT[Point] =
      {makepoint: (Real x Real) -> Point,
value point2: Point2 = pack[Point = (Real x Real) in
   Point2WRT[Point]] point1

Author: Wolfgang Schreiner
Last Modification: May 27, 1998

previous up next