]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tptp_grafite/ast.ml
the edges must be quoted as well (not only the nodes)
[helm.git] / helm / software / components / tptp_grafite / ast.ml
1 type kinds_of_formulae = 
2   | Axiom | Hypothesis | Definition | Lemma | Theorem | Conjecture
3   | Lemma_conjecture | Negated_conjecture | Plain | Unknown
4
5 type source = NoSource
6
7 type info = NoInfo
8
9 type term = 
10   | Variable of string
11   | Constant of string 
12   | Function of string * term list
13
14 type atom = 
15   | Proposition of string
16   | Predicate of string * term list
17   | True
18   | False
19   | Eq of term * term
20   | NotEq of term * term
21
22 type formulae = 
23   | Disjunction of formulae * formulae
24   | NegAtom of  atom
25   | Atom of atom
26   
27 type ast = 
28   | Comment of string
29   | Inclusion of string * (string list)
30   | AnnotatedFormula of 
31       string * kinds_of_formulae * formulae * source * info list