examples/mathtext/Logic.gf


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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 ; 
}