package electrod

  1. Overview
  2. Docs
constraint 'c = (Var.t, Tuple.t) CCList.Assoc.t
method visit_'v : (Var.t * Tuple.t) list -> Elo.var -> Elo.var
method visit_'i : (Var.t * Tuple.t) list -> Elo.ident -> Elo.ident
method build_fml : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Location.t -> Ltl.t
method build_Run : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.block -> Ltl.t list -> Ltl.t list
method build_True : (Var.t * Tuple.t) list -> Ltl.t
method build_False : (Var.t * Tuple.t) list -> Ltl.t
method build_Block : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.block -> Ltl.t list -> Ltl.t
method build_Let : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.binding list -> (Elo.var, Elo.ident) GenGoal.block -> (Elo.var * (Tuple.t -> Ltl.t)) list -> Ltl.t list -> Ltl.t
method build_Quant : (Var.t * Tuple.t) list -> G.quant -> (Elo.var, Elo.ident) G.sim_binding list -> (Elo.var, Elo.ident) GenGoal.block -> G.quant -> (GenGoal.disj * Elo.var list * (Tuple.t -> Ltl.t)) list -> Ltl.t list -> Ltl.t
method build_One : (Var.t * Tuple.t) list -> G.quant
method build_Lone : (Var.t * Tuple.t) list -> G.quant
method build_All : (Var.t * Tuple.t) list -> G.quant
method build_No : (Var.t * Tuple.t) list -> G.quant
method build_Some_ : (Var.t * Tuple.t) list -> G.quant
method build_And : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t -> Ltl.t
method build_Iff : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t -> Ltl.t
method build_Imp : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t -> Ltl.t
method build_U : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t -> Ltl.t
method build_Or : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t -> Ltl.t
method build_R : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t -> Ltl.t
method build_S : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t -> Ltl.t
method build_LUn : (Var.t * Tuple.t) list -> GenGoal.lunop -> (Elo.var, Elo.ident) GenGoal.fml -> ((Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t) -> Ltl.t -> Ltl.t
method build_X : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t
method build_F : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t
method build_G : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t
method build_H : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t
method build_O : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t
method build_P : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t
method build_Not : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t
method build_RComp : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> GenGoal.comp_op -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> ((Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Ltl.t
method build_REq : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Ltl.t
method build_In : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Ltl.t
method build_NotIn : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Ltl.t
method build_RNEq : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Ltl.t
method build_Gt : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t
method build_Gte : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t
method build_IEq : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t
method build_INEq : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t
method build_Lt : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t
method build_Lte : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t
method build_Qual : (Var.t * Tuple.t) list -> GenGoal.rqualify -> (Elo.var, Elo.ident) GenGoal.exp -> G.rqualify -> (Tuple.t -> Ltl.t) -> Ltl.t
method build_RLone : (Var.t * Tuple.t) list -> G.rqualify
method build_RNo : (Var.t * Tuple.t) list -> G.rqualify
method build_ROne : (Var.t * Tuple.t) list -> G.rqualify
method build_RSome : (Var.t * Tuple.t) list -> G.rqualify
method build_exp : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.exp -> (Tuple.t -> Ltl.t) -> Location.t -> int option -> Tuple.t -> Ltl.t
method visit_Compr : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.sim_binding list -> (Elo.var, Elo.ident) GenGoal.block -> Tuple.t -> Ltl.t
method private allocate_sbs_to_tuples : (Var.t * (Elo.var, Elo.ident) G.exp) Containers.List.t -> Atom.t Containers.List.t -> Tuple.t list
method build_Compr : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.sim_binding Containers.List.t -> (Elo.var, Elo.ident) GenGoal.block -> (GenGoal.disj * Elo.var list * (Tuple.t -> Ltl.t)) list -> Ltl.t list -> Tuple.t -> Ltl.t
method build_Iden : (Var.t * Tuple.t) list -> Tuple.t -> Ltl.t
method build_BoxJoin : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.exp -> (Elo.var, Elo.ident) GenGoal.exp list -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) list -> Tuple.t -> Ltl.t
method build_Ident : (Var.t * Tuple.t) list -> Elo.ident -> Elo.ident -> Tuple.t -> Ltl.t
method build_None_ : (Var.t * Tuple.t) list -> Tuple.t -> Ltl.t
method build_Univ : (Var.t * Tuple.t) list -> Tuple.t -> Ltl.t
method build_Prime : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.exp -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_RBin : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> GenGoal.rbinop -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> ((Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_Union : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_Inter : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_Join : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_LProj : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_RProj : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_Prod : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_Diff : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_Over : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_RUn : (Var.t * Tuple.t) list -> GenGoal.runop -> (Elo.var, Elo.ident) Elo.G.exp -> ((Elo.var, Elo.ident) Elo.G.exp -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t) -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_RTClos : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) Elo.G.exp -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_Transpose : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) Elo.G.exp -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_TClos : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) Elo.G.exp -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t
method build_iexp : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) GenGoal.iexp -> Ltl.term -> Location.t -> Ltl.term
method build_IUn : (Var.t * Tuple.t) list -> GenGoal.iunop -> (Elo.var, Elo.ident) GenGoal.iexp -> (Ltl.term -> Ltl.term) -> Ltl.term -> Ltl.term
method build_Num : (Var.t * Tuple.t) list -> int -> int -> Ltl.term
method build_Add : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.term
method build_Neg : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term
method build_Sub : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.term
method build_Card : (Var.t * Tuple.t) list -> (Elo.var, Elo.ident) G.exp -> (Tuple.t -> Ltl.t) -> Ltl.term
OCaml

Innovation. Community. Security.