Make (p.alt-ergo-lib.2.3.1.doc.alt-ergo-lib.AltErgoLib.Instances.Make)

Parameters

module X : Theory.S

Sourcetype t

Sourcetype tbox = X.t

Sourcetype instances = (Expr.gformula * Explanation.t) list

Sourceval empty : t

Sourceval add_terms : t -> Expr.Set.t -> Expr.gformula -> t

Sourceval add_lemma : t -> Expr.gformula -> Explanation.t -> t

Sourceval add_predicate : t -> Expr.gformula -> Explanation.t -> t

val m_lemmas : 
  Util.matching_env ->
  t ->
  tbox ->
  (Expr.t -> Expr.t -> bool) ->
  int ->
  instances * instances

val m_predicates : 
  Util.matching_env ->
  t ->
  tbox ->
  (Expr.t -> Expr.t -> bool) ->
  int ->
  instances * instances

Sourceval register_max_term_depth : t -> int -> t

val matching_terms_info : 
  t ->
  Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t