electrod 0.1.6 · OCaml Package

constraint 'c = Libelectrod__Elo_to_ltl1.stack

method private allocate_sbs_to_tuples : Libelectrod.Elo.exp Containers.List.t ->
  Libelectrod.Tuple.t ->
  Libelectrod.Tuple.t list

method build_Add : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_All : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method build_And : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Block : Libelectrod__Elo_to_ltl1.stack -> ltl list -> ltl

method build_Card : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  SMV_LTL.term

method build_Compr : Libelectrod__Elo_to_ltl1.stack ->
  (bool * int * Libelectrod.Elo.exp) list ->
  Libelectrod.Elo.fml list ->
  (bool * int * (Libelectrod.Tuple.t -> ltl)) list ->
  ltl list ->
  Libelectrod.Tuple.t ->
  ltl

method build_Diff : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_F : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_FIte : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  ltl ->
  ltl ->
  ltl ->
  ltl

method build_False : Libelectrod__Elo_to_ltl1.stack -> ltl

method build_G : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_Gt : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_Gte : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_H : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_IBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.ibinop ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term ->
  (SMV_LTL.term -> SMV_LTL.term -> SMV_LTL.term) ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_IComp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.icomp_op ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term ->
  SMV_LTL.tcomp ->
  SMV_LTL.term ->
  ltl

method build_IEq : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_INEq : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_IUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iunop ->
  Libelectrod.Elo.iexp ->
  (SMV_LTL.term -> SMV_LTL.term) ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_Iden : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method build_Iff : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Imp : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_In : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_Inter : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Join : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_LBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.lbinop ->
  Libelectrod.Elo.fml ->
  ltl ->
  (ltl -> ltl -> ltl) ->
  ltl ->
  ltl

method build_LProj : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_LUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.lunop ->
  Libelectrod.Elo.fml ->
  (ltl -> ltl) ->
  ltl ->
  ltl

method build_Lt : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_Lte : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_Name : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Name.t ->
  Libelectrod.Name.t ->
  Libelectrod.Tuple.t ->
  ltl

method build_Neg : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_No : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method build_None_ : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method build_Not : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_NotIn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_Num : Libelectrod__Elo_to_ltl1.stack -> int -> int -> SMV_LTL.term

method build_O : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_Or : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Over : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_P : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_Prime : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Prod : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Quant : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.quant ->
  (bool * int * Libelectrod.Elo.exp) ->
  Libelectrod.Elo.fml list ->
  Libelectrod.Elo.quant ->
  (bool * int * (Libelectrod.Tuple.t -> ltl)) ->
  ltl list ->
  ltl

method build_R : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_RBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.rbinop ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Elo.exp ->
    Libelectrod.Elo.exp ->
    (Libelectrod.Tuple.t -> ltl) ->
    (Libelectrod.Tuple.t -> ltl) ->
    Libelectrod.Tuple.t ->
    ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RComp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.comp_op ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Elo.exp ->
    Libelectrod.Elo.exp ->
    (Libelectrod.Tuple.t -> ltl) ->
    (Libelectrod.Tuple.t -> ltl) ->
    ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_REq : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_RIte : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  ltl ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RNEq : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_RProj : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RTClos : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.runop ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Elo.exp ->
    (Libelectrod.Tuple.t -> ltl) ->
    Libelectrod.Tuple.t ->
    ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_S : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Some_ : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method build_Sub : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_TClos : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Transpose : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_True : Libelectrod__Elo_to_ltl1.stack -> ltl

method build_U : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Union : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Univ : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method build_Var : Libelectrod__Elo_to_ltl1.stack ->
  int ->
  int ->
  Libelectrod.Tuple.t ->
  ltl

method build_X : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_oexp : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.oexp ->
  (Libelectrod.Tuple.t -> ltl) ->
  int ->
  Libelectrod.Tuple.t ->
  ltl

method private check_compr_disj : (bool * int * Libelectrod.Elo.exp) list ->
  Libelectrod.Tuple.t list ->
  bool

method visit_'exp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_'fml : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  ltl

method visit_'iexp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term

method visit_Add : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_All : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method visit_And : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Block : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml list ->
  ltl

method visit_Card : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  SMV_LTL.term

method visit_Compr : Libelectrod__Elo_to_ltl1.stack ->
  (bool * int * Libelectrod.Elo.exp) list ->
  Libelectrod.Elo.fml list ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Diff : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_F : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_FIte : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  ltl

method visit_False : Libelectrod__Elo_to_ltl1.stack -> ltl

method visit_G : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_Gt : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_Gte : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_H : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_IBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.ibinop ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term

method visit_IComp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.icomp_op ->
  Libelectrod.Elo.iexp ->
  ltl

method visit_IEq : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_INEq : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_IUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iunop ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term

method visit_Iden : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Iff : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Imp : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_In : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_Inter : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Join : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_LBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.lbinop ->
  Libelectrod.Elo.fml ->
  ltl

method visit_LProj : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_LUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.lunop ->
  Libelectrod.Elo.fml ->
  ltl

method visit_Lt : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_Lte : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_Name : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Name.t ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Neg : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_No : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method visit_None_ : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Not : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_NotIn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_Num : Libelectrod__Elo_to_ltl1.stack -> int -> SMV_LTL.term

method visit_O : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_Or : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Over : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_P : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_Prime : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Prod : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Quant : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.quant ->
  (bool * int * Libelectrod.Elo.exp) ->
  Libelectrod.Elo.fml list ->
  ltl

method visit_R : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_RBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.rbinop ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_RComp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.comp_op ->
  Libelectrod.Elo.exp ->
  ltl

method visit_REq : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_RIte : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_RNEq : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_RProj : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_RTClos : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_RUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.runop ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_S : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Some_ : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method visit_Sub : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_TClos : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Transpose : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_True : Libelectrod__Elo_to_ltl1.stack -> ltl

method visit_U : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Union : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Univ : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Var : Libelectrod__Elo_to_ltl1.stack ->
  int ->
  Libelectrod.Tuple.t ->
  ltl

method visit_X : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method private visit_array : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a array ->
  'b array

method private visit_bool : 'env. 'env -> bool -> bool

method private visit_bytes : 'env. 'env -> bytes -> bytes

method private visit_char : 'env. 'env -> char -> char

method visit_comp_op : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.comp_op ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_exp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method private visit_float : 'env. 'env -> float -> float

method visit_fml : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.fml -> ltl

method visit_ibinop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.ibinop ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_icomp_op : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.icomp_op ->
  SMV_LTL.tcomp

method visit_iexp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term

method private visit_int : 'env. 'env -> int -> int

method private visit_int32 : 'env. 'env -> int32 -> int32

method private visit_int64 : 'env. 'env -> int64 -> int64

method visit_iunop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iunop ->
  SMV_LTL.term ->
  SMV_LTL.term

method private visit_lazy_t : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a Stdlib.Lazy.t ->
  'b Stdlib.Lazy.t

method visit_lbinop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.lbinop ->
  ltl ->
  ltl ->
  ltl

method private visit_list : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a list ->
  'b list

method visit_lunop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.lunop ->
  ltl ->
  ltl

method private visit_nativeint : 'env. 'env -> nativeint -> nativeint

method visit_oexp : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.oexp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_ofml : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.ofml ->
  ltl

method visit_oiexp : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.oiexp ->
  SMV_LTL.term

method private visit_option : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a option ->
  'b option

method visit_prim_oexp : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.prim_oexp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_quant : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.quant ->
  Libelectrod.Elo.quant

method visit_rbinop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.rbinop ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method private visit_ref : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a Stdlib.ref ->
  'b Stdlib.ref

method private visit_result : 'env 'a 'b 'e 'f. ('env -> 'a -> 'b) ->
  ('env -> 'e -> 'f) ->
  'env ->
  ('a, 'e) Result.result ->
  ('b, 'f) Result.result

method visit_runop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.runop ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method private visit_string : 'env. 'env -> string -> string

method private visit_unit : 'env. 'env -> unit -> unit

package electrod