sig
  val equal : ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr -> bool
  val compare : ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr -> int
  val pp :
    ?env:string Syntax.Env.t ->
    'a Syntax.context -> Format.formatter -> ('a, 'b) Syntax.expr -> unit
  val refine :
    'a Syntax.context ->
    ('a, Syntax.typ_fo) Syntax.expr ->
    [ `Formula of 'a Syntax.formula | `Term of 'a Syntax.term ]
  module HT :
    sig
      type ('a, 'typ, 'b) t
      val create : int -> ('a, 'typ, 'b) Syntax.Expr.HT.t
      val add :
        ('a, 'typ, 'b) Syntax.Expr.HT.t ->
        ('a, 'typ) Syntax.expr -> 'b -> unit
      val replace :
        ('a, 'typ, 'b) Syntax.Expr.HT.t ->
        ('a, 'typ) Syntax.expr -> 'b -> unit
      val remove :
        ('a, 'typ, 'b) Syntax.Expr.HT.t -> ('a, 'typ) Syntax.expr -> unit
      val find :
        ('a, 'typ, 'b) Syntax.Expr.HT.t -> ('a, 'typ) Syntax.expr -> 'b
      val mem :
        ('a, 'typ, 'b) Syntax.Expr.HT.t -> ('a, 'typ) Syntax.expr -> bool
      val keys :
        ('a, 'typ, 'b) Syntax.Expr.HT.t -> ('a, 'typ) Syntax.expr BatEnum.t
      val values : ('a, 'typ, 'b) Syntax.Expr.HT.t -> 'b BatEnum.t
      val enum :
        ('a, 'typ, 'b) Syntax.Expr.HT.t ->
        (('a, 'typ) Syntax.expr * 'b) BatEnum.t
    end
  module Set :
    sig
      type ('a, 'typ) t
      val empty : ('a, 'typ) Syntax.Expr.Set.t
      val add :
        ('a, 'typ) Syntax.expr ->
        ('a, 'typ) Syntax.Expr.Set.t -> ('a, 'typ) Syntax.Expr.Set.t
      val union :
        ('a, 'typ) Syntax.Expr.Set.t ->
        ('a, 'typ) Syntax.Expr.Set.t -> ('a, 'typ) Syntax.Expr.Set.t
      val inter :
        ('a, 'typ) Syntax.Expr.Set.t ->
        ('a, 'typ) Syntax.Expr.Set.t -> ('a, 'typ) Syntax.Expr.Set.t
      val enum :
        ('a, 'typ) Syntax.Expr.Set.t -> ('a, 'typ) Syntax.expr BatEnum.t
      val mem :
        ('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.Expr.Set.t -> bool
    end
  module Map :
    sig
      type ('a, 'typ, 'b) t
      val empty : ('a, 'typ, 'b) Syntax.Expr.Map.t
      val is_empty : ('a, 'typ, 'b) Syntax.Expr.Map.t -> bool
      val add :
        ('a, 'typ) Syntax.expr ->
        'b ->
        ('a, 'typ, 'b) Syntax.Expr.Map.t -> ('a, 'typ, 'b) Syntax.Expr.Map.t
      val remove :
        ('a, 'typ) Syntax.expr ->
        ('a, 'typ, 'b) Syntax.Expr.Map.t -> ('a, 'typ, 'b) Syntax.Expr.Map.t
      val filter :
        (('a, 'typ) Syntax.expr -> 'b -> bool) ->
        ('a, 'typ, 'b) Syntax.Expr.Map.t -> ('a, 'typ, 'b) Syntax.Expr.Map.t
      val filter_map :
        (('a, 'typ) Syntax.expr -> 'b -> 'c option) ->
        ('a, 'typ, 'b) Syntax.Expr.Map.t -> ('a, 'typ, 'c) Syntax.Expr.Map.t
      val map :
        ('b -> 'c) ->
        ('a, 'typ, 'b) Syntax.Expr.Map.t -> ('a, 'typ, 'c) Syntax.Expr.Map.t
      val find :
        ('a, 'typ) Syntax.expr -> ('a, 'typ, 'b) Syntax.Expr.Map.t -> 'b
      val keys :
        ('a, 'typ, 'b) Syntax.Expr.Map.t -> ('a, 'typ) Syntax.expr BatEnum.t
      val values : ('a, 'typ, 'b) Syntax.Expr.Map.t -> 'b BatEnum.t
      val enum :
        ('a, 'typ, 'b) Syntax.Expr.Map.t ->
        (('a, 'typ) Syntax.expr * 'b) BatEnum.t
      val merge :
        (('a, 'typ) Syntax.expr -> 'b option -> 'c option -> 'd option) ->
        ('a, 'typ, 'b) Syntax.Expr.Map.t ->
        ('a, 'typ, 'c) Syntax.Expr.Map.t -> ('a, 'typ, 'd) Syntax.Expr.Map.t
      val fold :
        (('a, 'typ) Syntax.expr -> 'b -> 'c -> 'c) ->
        ('a, 'typ, 'b) Syntax.Expr.Map.t -> 'c -> 'c
    end
end