package alt-ergo-lib

  1. Overview
  2. Docs
type t
type theory
val empty : t
val make : max_t_depth:int -> Matching_types.info AltErgoLib.Expr.Map.t -> Expr.t list AltErgoLib.Expr.Map.t Symbols.Map.t -> Matching_types.trigger_info list -> t
val add_term : Matching_types.term_info -> Expr.t -> t -> t
val max_term_depth : t -> int -> t
val add_triggers : Util.matching_env -> t -> (Expr.t * int * Explanation.t) AltErgoLib.Expr.Map.t -> t
val terms_info : t -> Matching_types.info AltErgoLib.Expr.Map.t * Expr.t list AltErgoLib.Expr.Map.t Symbols.Map.t