msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

tutorial example of LF

Browse Source
This commit is contained in:
aarne
2006-06-16 08:06:52 +00:00
parent cb3dfbd9bf
commit be0e4d6203
1 changed files with 11 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
doc/tutorial/gf-tutorial2.txt
View File

@@ -1876,15 +1876,19 @@ In a logical framework, the formalization of a mathematical theory
is a set of type and function declarations. The following is an example is a set of type and function declarations. The following is an example
of such a theory, represented as an ``abstract`` module in GF. of such a theory, represented as an ``abstract`` module in GF.
``` ```
abstract Geometry = { abstract Arithm = {
cat cat
Line ; Point ; Circle ; -- basic types of figures Prop ; -- proposition
Prop ; -- proposition Nat ; -- natural number
fun fun
Parallel : Line -> Line -> Prop ; -- x is parallel to y Zero : Nat ; -- 0
Centre : Circle -> Point ; -- the centre of c Succ : Nat -> Nat ; -- successor of x
Even : Nat -> Prop ; -- x is even
And : Prop -> Prop -> Prop ; -- A and B
} }
``` ```
A concrete syntax is given below, as an example of using the resource grammar
library.