sig
  type cluster
  val cluster :
    id:string ->
    ?title:string -> ?position:Lexing.position -> unit -> Definitions.cluster
  val axiomatic : LogicUsage.axiomatic -> Definitions.cluster
  val section : LogicUsage.logic_section -> Definitions.cluster
  val compinfo : Cil_types.compinfo -> Definitions.cluster
  val matrix : Ctypes.c_object -> Definitions.cluster
  val cluster_id : Definitions.cluster -> string
  val cluster_title : Definitions.cluster -> string
  val cluster_position : Definitions.cluster -> Lexing.position option
  val cluster_age : Definitions.cluster -> int
  val cluster_compare : Definitions.cluster -> Definitions.cluster -> int
  val pp_cluster : Format.formatter -> Definitions.cluster -> unit
  val iter : (Definitions.cluster -> unit) -> unit
  type trigger = (Lang.F.var, Lang.lfun) Qed.Engine.ftrigger
  type typedef = (Lang.F.tau, Lang.field, Lang.lfun) Qed.Engine.ftypedef
  type dlemma = {
    l_name : string;
    l_cluster : Definitions.cluster;
    l_assumed : bool;
    l_types : int;
    l_forall : Lang.F.var list;
    l_triggers : Definitions.trigger list list;
    l_lemma : Lang.F.pred;
  }
  type definition =
      Logic of Lang.F.tau
    | Value of Lang.F.tau * Definitions.recursion * Lang.F.term
    | Predicate of Definitions.recursion * Lang.F.pred
    | Inductive of Definitions.dlemma list
  and recursion = Def | Rec
  type dfun = {
    d_lfun : Lang.lfun;
    d_cluster : Definitions.cluster;
    d_types : int;
    d_params : Lang.F.var list;
    d_definition : Definitions.definition;
  }
  module Trigger :
    sig
      val of_term : Lang.F.term -> Definitions.trigger
      val of_pred : Lang.F.pred -> Definitions.trigger
      val vars : Definitions.trigger -> Lang.F.Vars.t
    end
  val define_symbol : Definitions.dfun -> unit
  val update_symbol : Definitions.dfun -> unit
  val find_lemma : LogicUsage.logic_lemma -> Definitions.dlemma
  val compile_lemma :
    (LogicUsage.logic_lemma -> Definitions.dlemma) ->
    LogicUsage.logic_lemma -> unit
  val define_lemma : Definitions.dlemma -> unit
  val define_type : Definitions.cluster -> Cil_types.logic_type_info -> unit
  val call_fun :
    Lang.lfun ->
    (Lang.lfun -> Definitions.dfun) -> Lang.F.term list -> Lang.F.term
  val call_pred :
    Lang.lfun ->
    (Lang.lfun -> Definitions.dfun) -> Lang.F.term list -> Lang.F.pred
  type axioms = Definitions.cluster * LogicUsage.logic_lemma list
  class virtual visitor :
    Definitions.cluster ->
    object
      method do_local : Definitions.cluster -> bool
      method virtual on_cluster : Definitions.cluster -> unit
      method virtual on_comp :
        Cil_types.compinfo -> (Lang.field * Lang.F.tau) list -> unit
      method virtual on_dfun : Definitions.dfun -> unit
      method virtual on_dlemma : Definitions.dlemma -> unit
      method virtual on_library : string -> unit
      method virtual on_type :
        Cil_types.logic_type_info -> Definitions.typedef -> unit
      method virtual section : string -> unit
      method set_local : Definitions.cluster -> unit
      method vadt : Lang.F.ADT.t -> unit
      method vcluster : Definitions.cluster -> unit
      method vcomp : Cil_types.compinfo -> unit
      method vfield : Lang.F.Field.t -> unit
      method vgoal : Definitions.axioms option -> Lang.F.pred -> unit
      method vlemma : LogicUsage.logic_lemma -> unit
      method vlibrary : string -> unit
      method vparam : Lang.F.var -> unit
      method vpred : Lang.F.pred -> unit
      method vself : unit
      method vsymbol : Lang.lfun -> unit
      method vtau : Lang.F.tau -> unit
      method vterm : Lang.F.term -> unit
      method vtype : Cil_types.logic_type_info -> unit
    end
end