clauses.dk 363 Bytes
Newer Older
1 2 3
#NAME clauses.

atom : Type.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
4
mk_atom : p : fol.predicate -> fol.terms (fol.pred_domain p) -> atom.
5 6 7 8 9 10 11 12 13 14 15

litteral : Type.
pos_lit : atom -> litteral.
neg_lit : atom -> litteral.

clause : Type.
empty_clause : clause.
cons_clause : litteral -> clause -> clause.

qclause : Type.
qc_base : clause -> qclause.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
16
qc_all : A : fol.sort -> (fol.term A -> qclause) -> qclause.