previous up next
Go backward to A Rectangle Package
Go up to Top
Go forward to Bounded Quantification
RISC-Linz logo

A Figures Package

type FiguresWRT3[RectRep, CircleRep, PointRep] -
  {circlePackage: CircleWRT[CircleRep, PointRep],
   rectPackage: RectWRT[RectRep, PointRep],
   boundingRect: CircleRep -> RectRep}

type FIguresWRT1[PointRep] =
   exists RectRep. exists CircleRep.
      FigureWRT3[RectRep, CircleRep, PointRep]
type Figures = exists PointRep. FIgureWRT1[PointRep]
type FiguresModule = forall PointRep.
   PointWRT[PointRep] -> FiguresWRT1[PointRep]

value figuresModule: FIguresModule =
   fun(p: PointWRT[PointRep])
      pack[PointRep' = PointRep
         in FiguresWRT1[PointRep]]
      open circleModule[PointRep](p) as c[CircleRep] in
         open rectModule[PointRep](p) as r[RectRep] in
           {circlePackage = c, ...}

Author: Wolfgang Schreiner
Last Modification: May 27, 1998

previous up next