summaryrefslogtreecommitdiff
path: root/examples/math/Math.gf
diff options
context:
space:
mode:
authoraarne <aarne@cs.chalmers.se>2008-06-25 16:54:35 +0000
committeraarne <aarne@cs.chalmers.se>2008-06-25 16:54:35 +0000
commite9e80fc389365e24d4300d7d5390c7d833a96c50 (patch)
treef0b58473adaa670bd8fc52ada419d8cad470ee03 /examples/math/Math.gf
parentb96b36f43de3e2f8b58d5f539daa6f6d47f25870 (diff)
changed names of resource-1.3; added a note on homepage on release
Diffstat (limited to 'examples/math/Math.gf')
-rw-r--r--examples/math/Math.gf41
1 files changed, 0 insertions, 41 deletions
diff --git a/examples/math/Math.gf b/examples/math/Math.gf
deleted file mode 100644
index 35cfcbfdc..000000000
--- a/examples/math/Math.gf
+++ /dev/null
@@ -1,41 +0,0 @@
-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 ;
-
- V_x, V_y, V_z : Var ; --- for js
-
- 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 ;
-
-}