Go backward to Bounded Existential Quantification and Partial Abstraction Go up to Top Go 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}