clauses.dk 362 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
#NAME clauses.

atom : Type.
mk_atom : p : fol.predicate -> fol.terms (fol.pred_arity p) -> atom.

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.