forked from GitHub/gf-core
gf-book web page index and toc
This commit is contained in:
7
gf-book/examples/chapter8/Geometryb.gf
Normal file
7
gf-book/examples/chapter8/Geometryb.gf
Normal file
@@ -0,0 +1,7 @@
|
||||
abstract Geometry = Logic ** {
|
||||
fun
|
||||
Line, Point, Circle : Dom ;
|
||||
Intersect, Parallel : Ind -> Ind -> Prop ;
|
||||
Vertical : Ind -> Prop ;
|
||||
Centre : Ind -> Ind ;
|
||||
}
|
||||
Reference in New Issue
Block a user