aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/dp/fol.mli
blob: e42d1f224580ec3807eb20aeb1cf494d09abcb33 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

type typ =   Base of string
	   | Arrow of typ * typ
	   | Tuple of typ list

type term =   Cst of int
	    | Db of int
            | Tvar of string
            | Plus of term * term
	    | Moins of term * term
	    | Mult of term * term
	    | Div of term * term
	    | App of string * (term list)
and
     atom =   Eq of term * term
	    | Le of term * term
	    | Lt of term * term
	    | Ge of term * term
	    | Gt of term * term
            | Pred of string * (term list)
and
     form =   Fatom of atom
            | Fvar of string
	    | Imp of form * form
	    | And of form * form
	    | Or of form * form
	    | Not of form
	    | Forall of form
	    | Exists of form

type decl =
  | Assert of form
(*  | ...*)

type query = decl list * form