clauses.dk 359 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
literal : Type.
pos_lit : atom -> literal.
neg_lit : atom -> literal.
9 10 11

clause : Type.
empty_clause : clause.
12
cons_clause : literal -> clause -> clause.
13 14 15

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