gf-book/examples/chapter8/Logicb.gf


1
2
3
4
5
6
7
8
9
10
11

abstract Logic = {
cat
  Prop ; Ind ; Dom ; Var ; [Prop] {2} ; [Var] {1} ;
fun
  And, Or : [Prop] -> Prop ;
  If : Prop -> Prop -> Prop ;
  Not : Prop -> Prop ;
  All, Exist : [Var] -> Dom -> Prop -> Prop ;
  IVar : Var -> Ind ;
  VString : String -> Var ;
}