mathtext examples from Bonn

2009-12-18 11:08:39 +00:00
parent a4eb1800a4
commit c0de7a0627
24 changed files with 413 additions and 0 deletions
--- a/examples/mathtext/Logic.gf
+++ b/examples/mathtext/Logic.gf
@@ -0,0 +1,24 @@
+abstract Logic = Symbols ** {
+
+-- flags startcat = Prop ;
+
+cat
+  Prop ; Atom ; Ind ; Dom ; Var ; [Prop] {2} ; [Var] {1} ;
+fun
+  And, Or : [Prop] -> Prop ;
+  If, Iff : Prop -> Prop -> Prop ;
+  Not : Prop -> Prop ;
+  All, Exist : [Var] -> Dom -> Prop -> Prop ;
+  PAtom : Atom -> Prop ;
+  NAtom : Atom -> Prop ;
+  MkVar : String -> Var ;
+
+  PExp : Exp -> Prop ;
+  IExp : Exp -> Ind ;
+
+cat
+  Pred1 ; Pred2 ;
+fun 
+  PredPred1 : Pred1 -> Ind -> Atom ; 
+  PredPred2 : Pred2 -> Ind -> Ind -> Atom ; 
+}