GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-22 19:22:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

math wiki example

Browse Source
This commit is contained in:
aarne
2007-10-30 13:09:46 +00:00
parent af54ec7e45
commit 565bd85329
2 changed files with 82 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

39
examples/math/Math.gf Normal file
View File

@@ -0,0 +1,39 @@
abstract Math = {
flags startcat = Section ;
cat
Section ; Label ; Context ; Typ ; Obj ; Prop ; Proof ; Var ;
fun
SDefObj : Label -> Context -> Obj -> Typ -> Obj -> Section ;
SDefProp : Label -> Context -> Prop -> Prop -> Section ;
SAxiom : Label -> Context -> Prop -> Section ;
STheorem : Label -> Context -> Prop -> Proof -> Section ;
CEmpty : Context ;
CObj : Var -> Typ -> Context -> Context ;
CProp : Prop -> Context -> Context ;
OVar : Var -> Obj ;
LNone : Label ;
LString : String -> Label ;
VString : String -> Var ;
PLink : Proof ;
-- lexicon
Set : Typ ;
Nat : Typ ;
Zero : Obj ;
Succ : Obj -> Obj ;
One : Obj ;
Two : Obj ;
Even : Obj -> Prop ;
Odd : Obj -> Prop ;
Prime : Obj -> Prop ;
Divisible : Obj -> Obj -> Prop ;
}