Module Term.Rule

type t = rule
val lhs : t -> term
val rhs : t -> term
val vars : t -> Logtk.Term.VarSet.t
val vars_l : t -> Type.t HVar.t list
val head_id : t -> ID.t
val args : t -> term list
val arity : t -> int
val proof : t -> proof
val as_lit : t -> Literal.t
val make_const : proof:Proof.t -> ID.t -> Type.t -> term -> t

make_const id ty rhs is the same as T.const id ty --> rhs

val make : proof:Proof.t -> ID.t -> Type.t -> term list -> term -> t

make id ty args rhs is the same as T.app (T.const id ty) args --> rhs

include Interfaces.HASH with type t := t
include Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
type t
val compare : t -> t -> int
include Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string