Go backward to Bounded Existential Quantification and Partial AbstractionGo up to TopGo forward to Points and Tiles |

type Tile = `exists` P. `exists` T <= P. TileWRT2[P, T]

type TileWRT2[P, T] =

{mktile: (Int x Int x Int x Int) *->* T,

origin: T *->* P,

hor: T *->* Int,

ver: T *->* Int}

type TileWRT[P] = `exists` T <= P. TileWRT2[P, T]

type Tile = `exists` P. TileWRT[P]

type PointRep = {x: Int, y: Int}

type TileRep = {x: Int, y: Int, hor: Int, ver: Int}

Author: Wolfgang Schreiner

Last Modification: May 27, 1998