sig
type fact
and proof =
BuiltinProof
| InputFactProof
| Proof of Term.term * Fact.fact array
| DisjProof of int * Term.term * Fact.fact array * Fact.fact list
| NegProof of Term.term * Fact.fact array * Fact.fact
| UnknownProof
val null_fact : Fact.fact
val fact_with_unknown_proof : Fact.fact
val make_input_fact : Term.term -> Fact.fact
val make_derived_fact : Term.term -> Fact.fact
val make_derived_fact_with_proof : Term.term -> Fact.proof -> Fact.fact
val make_fact_like : Fact.fact -> Term.term -> Fact.fact
type entry = Fact.fact
val get_term : Fact.fact -> Term.term
val get_proof : Fact.fact -> Fact.proof
val proof_term_for_fact : Term.symbol_table -> Fact.fact -> Term.term
type l_proof = Fact.proof list
val proof_term_for_l_proof : Term.symbol_table -> Fact.l_proof -> Term.term
val make_subproofs : int -> Fact.fact array
type proof_term_aux
val make_proof_term_aux : unit -> Fact.proof_term_aux
val proof_term_for_r_proof :
Term.symbol_table -> Fact.proof_term_aux -> Fact.proof -> Term.term
end