Previous  Up  

Module Jst.Rel2


module Rel2: sig  end
Justifying ternary relations over pairs of terms.

type t = Term.t -> Term.t -> Jst.Three.t 
val apply : Jst.Eqtrans.t -> t -> t
Test binary term relation r on f a and f b.
Parameters:
f : Jst.Eqtrans.t
r : t
a : 'a
b : 'a
 
val orelse : t -> t -> t
Parameters:
r : t
s : t
a : 'a
b : 'b
 
val yes : Jst.Pred2.t -> t
Parameters:
p : Jst.Pred2.t
a : 'a
b : 'b
 
val no : Jst.Pred2.t -> t
Parameters:
p : Jst.Pred2.t
a : 'a
b : 'b
 
val yes_or_no : Jst.Pred2.t -> Jst.Pred2.t -> t
Parameters:
yes : Jst.Pred2.t
no : Jst.Pred2.t
a : 'a
b : 'b
 
val trace : Trace.level -> string -> t -> t
Parameters:
lvl : Trace.level
name : string
? : t