Go up to Top Go forward to Primitive Domains

Primitive Domains

• Truth values

  Domain Tr = B
  Operations

  true: Tr
  false:Tr
  not: Tr -> Tr
  or: Tr x Tr -> Tr
  (_ -> _ [] _): Tr x D x D -> D
      (for every domain D)

• Additional Nat operations

  equals: Nat x Nat -> Tr
  lessthan: Nat x Nat -> Tr
  greaterthan: Nat x Nat -> Tr

• One element domain

  Domain Unit, the one element-domain
  Operations (): Unit