Module Jst.Pred


module Pred: sig  end
Justifying predicates over terms.


type t = Term.t -> Jst.jst option
val disj : t -> t -> t
Disjunction.
Parameters:
p : t
q : t
a : 'a
val apply : Jst.Eqtrans.t -> t -> t
Test predicate p on f(a).
Parameters:
f : Jst.Eqtrans.t
p : t
a : 'a
val trace : Trace.level -> string -> t -> t
Parameters:
lvl : Trace.level
name : string
? : t