gf-book/examples/chapter9/LogicSymb.gf


1
2
3
4
5
6
7
8
9
10
11
12
13

concrete LogicSymb of Logic = open Formal, Prelude in {

lincat
  Prop, Ind = TermPrec ;
lin
  And = infixl 2 "\\&" ;
  Or  = infixl 2 "\\vee" ;
  If  = infixr 1 "\\sup" ;
  Not = prefix 3 "\\sim" ;
  All P = prefix 3 (parenth ("\\forall" ++ P.$0)) P ;
  Exist P = prefix 3 (parenth ("\\exists" ++ P.$0)) P ;
  Past = prefix 3 "P" ;
}