mathlib documentation

Return expr of proof that given int is negative

Return expr of proof that elements of (repeat 0 is.length) are all 0

Return expr of proof that the combination of linear constraints represented by ks and ts is unsatisfiable

Given a (([],les) : clause), return the expr of a term (t : clause.unsat ([],les)).

Given a (c : clause), return the expr of a term (t : clause.unsat c)

Given a (cs : list clause), return the expr of a term (t : clauses.unsat cs)