Go backward to Bounded Existential Quantification and Partial Abstraction
Go up to Top
Go forward to Points and Tiles

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}


Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: understand.tex,v 1.1 1996/06/12 09:38:21 schreine Exp schreine

Prev Up Next