previous up next
Go backward to Bounded Existential Quantification and Partial Abstraction
Go up to Top
Go forward to Points and Tiles
RISC-Linz logo

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

previous up next