path: root/gf-book/examples/chapter8/Geometryb.gf

abstract Geometry = Logic ** {
fun
  Line, Point, Circle : Dom ;
  Intersect, Parallel : Ind -> Ind -> Prop ;
  Vertical : Ind -> Prop ;
  Centre : Ind -> Ind ;
}