package point2
type Point is private;
function makepoint(x: Real, y: Real) return Point;
...
private
- - 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