Go backward to A Circle Package Go up to Top Go forward to A Figures Package |
type RectWRT2[RectRep, PointRep] =
{pointPackage: PointWRT[PointRep],
mkrect: (PointRep x PointRep) -> RectRep, ...}
type RectWRT1[PointRep] =
exists RectRep. RectWRT2[RectRep, PointRep]
type Rect = exists PointRep. RectWRT1[PointRep]
type RectModule = forall PointRep.
PointWRT[PointRep] -> RectWRT1[PointRep]
value rectModule: RectModule =
all[PointRep]
fun(p: PointWRT[PointRep])
pack[PointRep' = PointRep
in RectWRT1[PointRep']]
{pointPackage = p,
mkrect = fun(tl: PointRep, br: PointRep) ...}