electrod 0.1.4 · OCaml Package


  constraint
    < build_Add : 'd -> 'g
    ; build_All : 'd -> 'h
    ; build_And : 'd -> 'i
    ; build_Block : 'd -> ('j, 'k) GenGoal.block -> 'l list -> 'm
    ; build_BoxJoin : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      ('j, 'k) GenGoal.exp list ->
      'n ->
      'n list ->
      'o
    ; build_Card : 'd -> ('j, 'k) GenGoal.exp -> 'n -> 'p
    ; build_Compr : 
      'd ->
      ('j, 'k) GenGoal.sim_binding list ->
      ('j, 'k) GenGoal.block ->
      (GenGoal.disj * 'q list * 'n) list ->
      'l list ->
      'o
    ; build_Diff : 'd -> 'r -> 's -> 't
    ; build_F : 'd -> 'u
    ; build_FIte : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.fml ->
      'l ->
      'l ->
      'l ->
      'm
    ; build_False : 'd -> 'm
    ; build_G : 'd -> 'u
    ; build_Gt : 'd -> 'v
    ; build_Gte : 'd -> 'v
    ; build_H : 'd -> 'u
    ; build_IBin : 
      'd ->
      ('j, 'k) GenGoal.iexp ->
      GenGoal.ibinop ->
      ('j, 'k) GenGoal.iexp ->
      'w ->
      'g ->
      'w ->
      'p
    ; build_IComp : 
      'd ->
      ('j, 'k) GenGoal.iexp ->
      GenGoal.icomp_op ->
      ('j, 'k) GenGoal.iexp ->
      'w ->
      'v ->
      'w ->
      'm
    ; build_IEq : 'd -> 'v
    ; build_INEq : 'd -> 'v
    ; build_IUn : 
      'd ->
      GenGoal.iunop ->
      ('j, 'k) GenGoal.iexp ->
      'x ->
      'w ->
      'p
    ; build_Iden : 'd -> 'o
    ; build_Ident : 'd -> 'k -> 'y -> 'o
    ; build_Iff : 'd -> 'i
    ; build_Imp : 'd -> 'i
    ; build_In : 'd -> 'z
    ; build_Inter : 'd -> 'r -> 's -> 't
    ; build_Join : 'd -> 'r -> 's -> 't
    ; build_LBin : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      GenGoal.lbinop ->
      ('j, 'k) GenGoal.fml ->
      'l ->
      'i ->
      'l ->
      'm
    ; build_LProj : 'd -> 'r -> 's -> 't
    ; build_LUn : 'd -> GenGoal.lunop -> ('j, 'k) GenGoal.fml -> 'u -> 'l -> 'm
    ; build_Let : 
      'd ->
      ('j, 'k) GenGoal.binding list ->
      ('j, 'k) GenGoal.block ->
      ('q * 'n) list ->
      'l list ->
      'm
    ; build_Lone : 'd -> 'h
    ; build_Lt : 'd -> 'v
    ; build_Lte : 'd -> 'v
    ; build_Neg : 'd -> 'x
    ; build_No : 'd -> 'h
    ; build_None_ : 'd -> 'o
    ; build_Not : 'd -> 'u
    ; build_NotIn : 'd -> 'z
    ; build_Num : 'd -> int -> int -> 'p
    ; build_O : 'd -> 'u
    ; build_One : 'd -> 'h
    ; build_Or : 'd -> 'i
    ; build_Over : 'd -> 'r -> 's -> 't
    ; build_P : 'd -> 'u
    ; build_Prime : 'd -> ('j, 'k) GenGoal.exp -> 'n -> 'o
    ; build_Prod : 'd -> 'r -> 's -> 't
    ; build_Qual : 
      'd ->
      GenGoal.rqualify ->
      ('j, 'k) GenGoal.exp ->
      'a1 ->
      'n ->
      'm
    ; build_Quant : 
      'd ->
      GenGoal.quant ->
      ('j, 'k) GenGoal.sim_binding list ->
      ('j, 'k) GenGoal.block ->
      'h ->
      (GenGoal.disj * 'q list * 'n) list ->
      'l list ->
      'm
    ; build_R : 'd -> 'i
    ; build_RBin : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      GenGoal.rbinop ->
      ('j, 'k) GenGoal.exp ->
      'n ->
      ('r -> 's -> 't) ->
      'n ->
      'o
    ; build_RComp : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      GenGoal.comp_op ->
      ('j, 'k) GenGoal.exp ->
      'n ->
      'z ->
      'n ->
      'm
    ; build_REq : 'd -> 'z
    ; build_RIte : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.exp ->
      ('j, 'k) GenGoal.exp ->
      'l ->
      'n ->
      'n ->
      'o
    ; build_RLone : 'd -> 'a1
    ; build_RNEq : 'd -> 'z
    ; build_RNo : 'd -> 'a1
    ; build_ROne : 'd -> 'a1
    ; build_RProj : 'd -> 'r -> 's -> 't
    ; build_RSome : 'd -> 'a1
    ; build_RTClos : 'd -> 'b1
    ; build_RUn : 
      'd ->
      GenGoal.runop ->
      ('j, 'k) GenGoal.exp ->
      'b1 ->
      'n ->
      'o
    ; build_Run : 'd -> ('j, 'k) GenGoal.block -> 'l list -> 'c1
    ; build_S : 'd -> 'i
    ; build_Some_ : 'd -> 'h
    ; build_Sub : 'd -> 'g
    ; build_TClos : 'd -> 'b1
    ; build_Transpose : 'd -> 'b1
    ; build_True : 'd -> 'm
    ; build_U : 'd -> 'i
    ; build_Union : 'd -> 'r -> 's -> 't
    ; build_Univ : 'd -> 'o
    ; build_X : 'd -> 'u
    ; build_exp : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      'o ->
      Location.t ->
      int option ->
      'n
    ; build_fml : 'd -> ('j, 'k) GenGoal.fml -> 'm -> Location.t -> 'l
    ; build_iexp : 'd -> ('j, 'k) GenGoal.iexp -> 'p -> Location.t -> 'w
    ; visit_'i : 'd -> 'k -> 'y
    ; visit_'v : 'd -> 'j -> 'q
    ; visit_Add : 'd -> 'g
    ; visit_All : 'd -> 'h
    ; visit_And : 'd -> 'i
    ; visit_Block : 'd -> ('j, 'k) GenGoal.block -> 'm
    ; visit_BoxJoin : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      ('j, 'k) GenGoal.exp list ->
      'o
    ; visit_Card : 'd -> ('j, 'k) GenGoal.exp -> 'p
    ; visit_Compr : 
      'd ->
      ('j, 'k) GenGoal.sim_binding list ->
      ('j, 'k) GenGoal.block ->
      'o
    ; visit_Diff : 'd -> 'r -> 's -> 't
    ; visit_F : 'd -> 'u
    ; visit_FIte : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.fml ->
      'm
    ; visit_False : 'd -> 'm
    ; visit_G : 'd -> 'u
    ; visit_Gt : 'd -> 'v
    ; visit_Gte : 'd -> 'v
    ; visit_H : 'd -> 'u
    ; visit_IBin : 
      'd ->
      ('j, 'k) GenGoal.iexp ->
      GenGoal.ibinop ->
      ('j, 'k) GenGoal.iexp ->
      'p
    ; visit_IComp : 
      'd ->
      ('j, 'k) GenGoal.iexp ->
      GenGoal.icomp_op ->
      ('j, 'k) GenGoal.iexp ->
      'm
    ; visit_IEq : 'd -> 'v
    ; visit_INEq : 'd -> 'v
    ; visit_IUn : 'd -> GenGoal.iunop -> ('j, 'k) GenGoal.iexp -> 'p
    ; visit_Iden : 'd -> 'o
    ; visit_Ident : 'd -> 'k -> 'o
    ; visit_Iff : 'd -> 'i
    ; visit_Imp : 'd -> 'i
    ; visit_In : 'd -> 'z
    ; visit_Inter : 'd -> 'r -> 's -> 't
    ; visit_Join : 'd -> 'r -> 's -> 't
    ; visit_LBin : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      GenGoal.lbinop ->
      ('j, 'k) GenGoal.fml ->
      'm
    ; visit_LProj : 'd -> 'r -> 's -> 't
    ; visit_LUn : 'd -> GenGoal.lunop -> ('j, 'k) GenGoal.fml -> 'm
    ; visit_Let : 
      'd ->
      ('j, 'k) GenGoal.binding list ->
      ('j, 'k) GenGoal.block ->
      'm
    ; visit_Lone : 'd -> 'h
    ; visit_Lt : 'd -> 'v
    ; visit_Lte : 'd -> 'v
    ; visit_Neg : 'd -> 'x
    ; visit_No : 'd -> 'h
    ; visit_None_ : 'd -> 'o
    ; visit_Not : 'd -> 'u
    ; visit_NotIn : 'd -> 'z
    ; visit_Num : 'd -> int -> 'p
    ; visit_O : 'd -> 'u
    ; visit_One : 'd -> 'h
    ; visit_Or : 'd -> 'i
    ; visit_Over : 'd -> 'r -> 's -> 't
    ; visit_P : 'd -> 'u
    ; visit_Prime : 'd -> ('j, 'k) GenGoal.exp -> 'o
    ; visit_Prod : 'd -> 'r -> 's -> 't
    ; visit_Qual : 'd -> GenGoal.rqualify -> ('j, 'k) GenGoal.exp -> 'm
    ; visit_Quant : 
      'd ->
      GenGoal.quant ->
      ('j, 'k) GenGoal.sim_binding list ->
      ('j, 'k) GenGoal.block ->
      'm
    ; visit_R : 'd -> 'i
    ; visit_RBin : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      GenGoal.rbinop ->
      ('j, 'k) GenGoal.exp ->
      'o
    ; visit_RComp : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      GenGoal.comp_op ->
      ('j, 'k) GenGoal.exp ->
      'm
    ; visit_REq : 'd -> 'z
    ; visit_RIte : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.exp ->
      ('j, 'k) GenGoal.exp ->
      'o
    ; visit_RLone : 'd -> 'a1
    ; visit_RNEq : 'd -> 'z
    ; visit_RNo : 'd -> 'a1
    ; visit_ROne : 'd -> 'a1
    ; visit_RProj : 'd -> 'r -> 's -> 't
    ; visit_RSome : 'd -> 'a1
    ; visit_RTClos : 'd -> 'b1
    ; visit_RUn : 'd -> GenGoal.runop -> ('j, 'k) GenGoal.exp -> 'o
    ; visit_Run : 'd -> ('j, 'k) GenGoal.block -> 'c1
    ; visit_S : 'd -> 'i
    ; visit_Some_ : 'd -> 'h
    ; visit_Sub : 'd -> 'g
    ; visit_TClos : 'd -> 'b1
    ; visit_Transpose : 'd -> 'b1
    ; visit_True : 'd -> 'm
    ; visit_U : 'd -> 'i
    ; visit_Union : 'd -> 'r -> 's -> 't
    ; visit_Univ : 'd -> 'o
    ; visit_X : 'd -> 'u
    ; visit_binding : 'd -> ('j, 'k) GenGoal.binding -> 'q * 'n
    ; visit_block : 'd -> ('j, 'k) GenGoal.block -> 'l list
    ; visit_comp_op : 'd -> GenGoal.comp_op -> 'z
    ; visit_disj : 'd -> GenGoal.disj -> GenGoal.disj
    ; visit_exp : 'd -> ('j, 'k) GenGoal.exp -> 'n
    ; visit_fml : 'd -> ('j, 'k) GenGoal.fml -> 'l
    ; visit_ibinop : 'd -> GenGoal.ibinop -> 'g
    ; visit_icomp_op : 'd -> GenGoal.icomp_op -> 'v
    ; visit_iexp : 'd -> ('j, 'k) GenGoal.iexp -> 'w
    ; visit_iunop : 'd -> GenGoal.iunop -> 'x
    ; visit_lbinop : 'd -> GenGoal.lbinop -> 'i
    ; visit_lunop : 'd -> GenGoal.lunop -> 'u
    ; visit_prim_exp : 'd -> ('j, 'k) GenGoal.prim_exp -> 'o
    ; visit_prim_fml : 'd -> ('j, 'k) GenGoal.prim_fml -> 'm
    ; visit_prim_iexp : 'd -> ('j, 'k) GenGoal.prim_iexp -> 'p
    ; visit_quant : 'd -> GenGoal.quant -> 'h
    ; visit_rbinop : 'd -> GenGoal.rbinop -> 'r -> 's -> 't
    ; visit_rqualify : 'd -> GenGoal.rqualify -> 'a1
    ; visit_runop : 'd -> GenGoal.runop -> 'b1
    ; visit_sim_binding : 
      'd ->
      ('j, 'k) GenGoal.sim_binding ->
      GenGoal.disj * 'q list * 'n
    ; visit_t : 'd -> ('j, 'k) GenGoal.t -> 'c1.. > =
    < build_Add : 'd -> 'g
    ; build_All : 'd -> 'h
    ; build_And : 'd -> 'i
    ; build_Block : 'd -> ('j, 'k) GenGoal.block -> 'l list -> 'm
    ; build_BoxJoin : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      ('j, 'k) GenGoal.exp list ->
      'n ->
      'n list ->
      'o
    ; build_Card : 'd -> ('j, 'k) GenGoal.exp -> 'n -> 'p
    ; build_Compr : 
      'd ->
      ('j, 'k) GenGoal.sim_binding list ->
      ('j, 'k) GenGoal.block ->
      (GenGoal.disj * 'q list * 'n) list ->
      'l list ->
      'o
    ; build_Diff : 'd -> 'r -> 's -> 't
    ; build_F : 'd -> 'u
    ; build_FIte : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.fml ->
      'l ->
      'l ->
      'l ->
      'm
    ; build_False : 'd -> 'm
    ; build_G : 'd -> 'u
    ; build_Gt : 'd -> 'v
    ; build_Gte : 'd -> 'v
    ; build_H : 'd -> 'u
    ; build_IBin : 
      'd ->
      ('j, 'k) GenGoal.iexp ->
      GenGoal.ibinop ->
      ('j, 'k) GenGoal.iexp ->
      'w ->
      'g ->
      'w ->
      'p
    ; build_IComp : 
      'd ->
      ('j, 'k) GenGoal.iexp ->
      GenGoal.icomp_op ->
      ('j, 'k) GenGoal.iexp ->
      'w ->
      'v ->
      'w ->
      'm
    ; build_IEq : 'd -> 'v
    ; build_INEq : 'd -> 'v
    ; build_IUn : 
      'd ->
      GenGoal.iunop ->
      ('j, 'k) GenGoal.iexp ->
      'x ->
      'w ->
      'p
    ; build_Iden : 'd -> 'o
    ; build_Ident : 'd -> 'k -> 'y -> 'o
    ; build_Iff : 'd -> 'i
    ; build_Imp : 'd -> 'i
    ; build_In : 'd -> 'z
    ; build_Inter : 'd -> 'r -> 's -> 't
    ; build_Join : 'd -> 'r -> 's -> 't
    ; build_LBin : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      GenGoal.lbinop ->
      ('j, 'k) GenGoal.fml ->
      'l ->
      'i ->
      'l ->
      'm
    ; build_LProj : 'd -> 'r -> 's -> 't
    ; build_LUn : 'd -> GenGoal.lunop -> ('j, 'k) GenGoal.fml -> 'u -> 'l -> 'm
    ; build_Let : 
      'd ->
      ('j, 'k) GenGoal.binding list ->
      ('j, 'k) GenGoal.block ->
      ('q * 'n) list ->
      'l list ->
      'm
    ; build_Lone : 'd -> 'h
    ; build_Lt : 'd -> 'v
    ; build_Lte : 'd -> 'v
    ; build_Neg : 'd -> 'x
    ; build_No : 'd -> 'h
    ; build_None_ : 'd -> 'o
    ; build_Not : 'd -> 'u
    ; build_NotIn : 'd -> 'z
    ; build_Num : 'd -> int -> int -> 'p
    ; build_O : 'd -> 'u
    ; build_One : 'd -> 'h
    ; build_Or : 'd -> 'i
    ; build_Over : 'd -> 'r -> 's -> 't
    ; build_P : 'd -> 'u
    ; build_Prime : 'd -> ('j, 'k) GenGoal.exp -> 'n -> 'o
    ; build_Prod : 'd -> 'r -> 's -> 't
    ; build_Qual : 
      'd ->
      GenGoal.rqualify ->
      ('j, 'k) GenGoal.exp ->
      'a1 ->
      'n ->
      'm
    ; build_Quant : 
      'd ->
      GenGoal.quant ->
      ('j, 'k) GenGoal.sim_binding list ->
      ('j, 'k) GenGoal.block ->
      'h ->
      (GenGoal.disj * 'q list * 'n) list ->
      'l list ->
      'm
    ; build_R : 'd -> 'i
    ; build_RBin : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      GenGoal.rbinop ->
      ('j, 'k) GenGoal.exp ->
      'n ->
      ('r -> 's -> 't) ->
      'n ->
      'o
    ; build_RComp : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      GenGoal.comp_op ->
      ('j, 'k) GenGoal.exp ->
      'n ->
      'z ->
      'n ->
      'm
    ; build_REq : 'd -> 'z
    ; build_RIte : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.exp ->
      ('j, 'k) GenGoal.exp ->
      'l ->
      'n ->
      'n ->
      'o
    ; build_RLone : 'd -> 'a1
    ; build_RNEq : 'd -> 'z
    ; build_RNo : 'd -> 'a1
    ; build_ROne : 'd -> 'a1
    ; build_RProj : 'd -> 'r -> 's -> 't
    ; build_RSome : 'd -> 'a1
    ; build_RTClos : 'd -> 'b1
    ; build_RUn : 
      'd ->
      GenGoal.runop ->
      ('j, 'k) GenGoal.exp ->
      'b1 ->
      'n ->
      'o
    ; build_Run : 'd -> ('j, 'k) GenGoal.block -> 'l list -> 'c1
    ; build_S : 'd -> 'i
    ; build_Some_ : 'd -> 'h
    ; build_Sub : 'd -> 'g
    ; build_TClos : 'd -> 'b1
    ; build_Transpose : 'd -> 'b1
    ; build_True : 'd -> 'm
    ; build_U : 'd -> 'i
    ; build_Union : 'd -> 'r -> 's -> 't
    ; build_Univ : 'd -> 'o
    ; build_X : 'd -> 'u
    ; build_exp : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      'o ->
      Location.t ->
      int option ->
      'n
    ; build_fml : 'd -> ('j, 'k) GenGoal.fml -> 'm -> Location.t -> 'l
    ; build_iexp : 'd -> ('j, 'k) GenGoal.iexp -> 'p -> Location.t -> 'w
    ; visit_'i : 'd -> 'k -> 'y
    ; visit_'v : 'd -> 'j -> 'q
    ; visit_Add : 'd -> 'g
    ; visit_All : 'd -> 'h
    ; visit_And : 'd -> 'i
    ; visit_Block : 'd -> ('j, 'k) GenGoal.block -> 'm
    ; visit_BoxJoin : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      ('j, 'k) GenGoal.exp list ->
      'o
    ; visit_Card : 'd -> ('j, 'k) GenGoal.exp -> 'p
    ; visit_Compr : 
      'd ->
      ('j, 'k) GenGoal.sim_binding list ->
      ('j, 'k) GenGoal.block ->
      'o
    ; visit_Diff : 'd -> 'r -> 's -> 't
    ; visit_F : 'd -> 'u
    ; visit_FIte : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.fml ->
      'm
    ; visit_False : 'd -> 'm
    ; visit_G : 'd -> 'u
    ; visit_Gt : 'd -> 'v
    ; visit_Gte : 'd -> 'v
    ; visit_H : 'd -> 'u
    ; visit_IBin : 
      'd ->
      ('j, 'k) GenGoal.iexp ->
      GenGoal.ibinop ->
      ('j, 'k) GenGoal.iexp ->
      'p
    ; visit_IComp : 
      'd ->
      ('j, 'k) GenGoal.iexp ->
      GenGoal.icomp_op ->
      ('j, 'k) GenGoal.iexp ->
      'm
    ; visit_IEq : 'd -> 'v
    ; visit_INEq : 'd -> 'v
    ; visit_IUn : 'd -> GenGoal.iunop -> ('j, 'k) GenGoal.iexp -> 'p
    ; visit_Iden : 'd -> 'o
    ; visit_Ident : 'd -> 'k -> 'o
    ; visit_Iff : 'd -> 'i
    ; visit_Imp : 'd -> 'i
    ; visit_In : 'd -> 'z
    ; visit_Inter : 'd -> 'r -> 's -> 't
    ; visit_Join : 'd -> 'r -> 's -> 't
    ; visit_LBin : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      GenGoal.lbinop ->
      ('j, 'k) GenGoal.fml ->
      'm
    ; visit_LProj : 'd -> 'r -> 's -> 't
    ; visit_LUn : 'd -> GenGoal.lunop -> ('j, 'k) GenGoal.fml -> 'm
    ; visit_Let : 
      'd ->
      ('j, 'k) GenGoal.binding list ->
      ('j, 'k) GenGoal.block ->
      'm
    ; visit_Lone : 'd -> 'h
    ; visit_Lt : 'd -> 'v
    ; visit_Lte : 'd -> 'v
    ; visit_Neg : 'd -> 'x
    ; visit_No : 'd -> 'h
    ; visit_None_ : 'd -> 'o
    ; visit_Not : 'd -> 'u
    ; visit_NotIn : 'd -> 'z
    ; visit_Num : 'd -> int -> 'p
    ; visit_O : 'd -> 'u
    ; visit_One : 'd -> 'h
    ; visit_Or : 'd -> 'i
    ; visit_Over : 'd -> 'r -> 's -> 't
    ; visit_P : 'd -> 'u
    ; visit_Prime : 'd -> ('j, 'k) GenGoal.exp -> 'o
    ; visit_Prod : 'd -> 'r -> 's -> 't
    ; visit_Qual : 'd -> GenGoal.rqualify -> ('j, 'k) GenGoal.exp -> 'm
    ; visit_Quant : 
      'd ->
      GenGoal.quant ->
      ('j, 'k) GenGoal.sim_binding list ->
      ('j, 'k) GenGoal.block ->
      'm
    ; visit_R : 'd -> 'i
    ; visit_RBin : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      GenGoal.rbinop ->
      ('j, 'k) GenGoal.exp ->
      'o
    ; visit_RComp : 
      'd ->
      ('j, 'k) GenGoal.exp ->
      GenGoal.comp_op ->
      ('j, 'k) GenGoal.exp ->
      'm
    ; visit_REq : 'd -> 'z
    ; visit_RIte : 
      'd ->
      ('j, 'k) GenGoal.fml ->
      ('j, 'k) GenGoal.exp ->
      ('j, 'k) GenGoal.exp ->
      'o
    ; visit_RLone : 'd -> 'a1
    ; visit_RNEq : 'd -> 'z
    ; visit_RNo : 'd -> 'a1
    ; visit_ROne : 'd -> 'a1
    ; visit_RProj : 'd -> 'r -> 's -> 't
    ; visit_RSome : 'd -> 'a1
    ; visit_RTClos : 'd -> 'b1
    ; visit_RUn : 'd -> GenGoal.runop -> ('j, 'k) GenGoal.exp -> 'o
    ; visit_Run : 'd -> ('j, 'k) GenGoal.block -> 'c1
    ; visit_S : 'd -> 'i
    ; visit_Some_ : 'd -> 'h
    ; visit_Sub : 'd -> 'g
    ; visit_TClos : 'd -> 'b1
    ; visit_Transpose : 'd -> 'b1
    ; visit_True : 'd -> 'm
    ; visit_U : 'd -> 'i
    ; visit_Union : 'd -> 'r -> 's -> 't
    ; visit_Univ : 'd -> 'o
    ; visit_X : 'd -> 'u
    ; visit_binding : 'd -> ('j, 'k) GenGoal.binding -> 'q * 'n
    ; visit_block : 'd -> ('j, 'k) GenGoal.block -> 'l list
    ; visit_comp_op : 'd -> GenGoal.comp_op -> 'z
    ; visit_disj : 'd -> GenGoal.disj -> GenGoal.disj
    ; visit_exp : 'd -> ('j, 'k) GenGoal.exp -> 'n
    ; visit_fml : 'd -> ('j, 'k) GenGoal.fml -> 'l
    ; visit_ibinop : 'd -> GenGoal.ibinop -> 'g
    ; visit_icomp_op : 'd -> GenGoal.icomp_op -> 'v
    ; visit_iexp : 'd -> ('j, 'k) GenGoal.iexp -> 'w
    ; visit_iunop : 'd -> GenGoal.iunop -> 'x
    ; visit_lbinop : 'd -> GenGoal.lbinop -> 'i
    ; visit_lunop : 'd -> GenGoal.lunop -> 'u
    ; visit_prim_exp : 'd -> ('j, 'k) GenGoal.prim_exp -> 'o
    ; visit_prim_fml : 'd -> ('j, 'k) GenGoal.prim_fml -> 'm
    ; visit_prim_iexp : 'd -> ('j, 'k) GenGoal.prim_iexp -> 'p
    ; visit_quant : 'd -> GenGoal.quant -> 'h
    ; visit_rbinop : 'd -> GenGoal.rbinop -> 'r -> 's -> 't
    ; visit_rqualify : 'd -> GenGoal.rqualify -> 'a1
    ; visit_runop : 'd -> GenGoal.runop -> 'b1
    ; visit_sim_binding : 
      'd ->
      ('j, 'k) GenGoal.sim_binding ->
      GenGoal.disj * 'q list * 'n
    ; visit_t : 'd -> ('j, 'k) GenGoal.t -> 'c1.. >

inherit VisitorsRuntime.map

method virtual build_Add : 'd -> 'g

method virtual build_All : 'd -> 'h

method virtual build_And : 'd -> 'i

method virtual build_Block : 'd -> ('j, 'k) GenGoal.block -> 'l list -> 'm

method virtual build_BoxJoin : 'd ->
  ('j, 'k) GenGoal.exp ->
  ('j, 'k) GenGoal.exp list ->
  'n ->
  'n list ->
  'o

method virtual build_Card : 'd -> ('j, 'k) GenGoal.exp -> 'n -> 'p

method virtual build_Compr : 'd ->
  ('j, 'k) GenGoal.sim_binding list ->
  ('j, 'k) GenGoal.block ->
  (GenGoal.disj * 'q list * 'n) list ->
  'l list ->
  'o

method virtual build_Diff : 'd -> 'r -> 's -> 't

method virtual build_F : 'd -> 'u

method virtual build_FIte : 'd ->
  ('j, 'k) GenGoal.fml ->
  ('j, 'k) GenGoal.fml ->
  ('j, 'k) GenGoal.fml ->
  'l ->
  'l ->
  'l ->
  'm

method virtual build_False : 'd -> 'm

method virtual build_G : 'd -> 'u

method virtual build_Gt : 'd -> 'v

method virtual build_Gte : 'd -> 'v

method virtual build_H : 'd -> 'u

method virtual build_IBin : 'd ->
  ('j, 'k) GenGoal.iexp ->
  GenGoal.ibinop ->
  ('j, 'k) GenGoal.iexp ->
  'w ->
  'g ->
  'w ->
  'p

method virtual build_IComp : 'd ->
  ('j, 'k) GenGoal.iexp ->
  GenGoal.icomp_op ->
  ('j, 'k) GenGoal.iexp ->
  'w ->
  'v ->
  'w ->
  'm

method virtual build_IEq : 'd -> 'v

method virtual build_INEq : 'd -> 'v

method virtual build_IUn : 'd ->
  GenGoal.iunop ->
  ('j, 'k) GenGoal.iexp ->
  'x ->
  'w ->
  'p

method virtual build_Iden : 'd -> 'o

method virtual build_Ident : 'd -> 'k -> 'y -> 'o

method virtual build_Iff : 'd -> 'i

method virtual build_Imp : 'd -> 'i

method virtual build_In : 'd -> 'z

method virtual build_Inter : 'd -> 'r -> 's -> 't

method virtual build_Join : 'd -> 'r -> 's -> 't

method virtual build_LBin : 'd ->
  ('j, 'k) GenGoal.fml ->
  GenGoal.lbinop ->
  ('j, 'k) GenGoal.fml ->
  'l ->
  'i ->
  'l ->
  'm

method virtual build_LProj : 'd -> 'r -> 's -> 't

method virtual build_LUn : 'd ->
  GenGoal.lunop ->
  ('j, 'k) GenGoal.fml ->
  'u ->
  'l ->
  'm

method virtual build_Let : 'd ->
  ('j, 'k) GenGoal.binding list ->
  ('j, 'k) GenGoal.block ->
  ('q * 'n) list ->
  'l list ->
  'm

method virtual build_Lone : 'd -> 'h

method virtual build_Lt : 'd -> 'v

method virtual build_Lte : 'd -> 'v

method virtual build_Neg : 'd -> 'x

method virtual build_No : 'd -> 'h

method virtual build_None_ : 'd -> 'o

method virtual build_Not : 'd -> 'u

method virtual build_NotIn : 'd -> 'z

method virtual build_Num : 'd -> int -> int -> 'p

method virtual build_O : 'd -> 'u

method virtual build_One : 'd -> 'h

method virtual build_Or : 'd -> 'i

method virtual build_Over : 'd -> 'r -> 's -> 't

method virtual build_P : 'd -> 'u

method virtual build_Prime : 'd -> ('j, 'k) GenGoal.exp -> 'n -> 'o

method virtual build_Prod : 'd -> 'r -> 's -> 't

method virtual build_Qual : 'd ->
  GenGoal.rqualify ->
  ('j, 'k) GenGoal.exp ->
  'a1 ->
  'n ->
  'm

method virtual build_Quant : 'd ->
  GenGoal.quant ->
  ('j, 'k) GenGoal.sim_binding list ->
  ('j, 'k) GenGoal.block ->
  'h ->
  (GenGoal.disj * 'q list * 'n) list ->
  'l list ->
  'm

method virtual build_R : 'd -> 'i

method virtual build_RBin : 'd ->
  ('j, 'k) GenGoal.exp ->
  GenGoal.rbinop ->
  ('j, 'k) GenGoal.exp ->
  'n ->
  ('r -> 's -> 't) ->
  'n ->
  'o

method virtual build_RComp : 'd ->
  ('j, 'k) GenGoal.exp ->
  GenGoal.comp_op ->
  ('j, 'k) GenGoal.exp ->
  'n ->
  'z ->
  'n ->
  'm

method virtual build_REq : 'd -> 'z

method virtual build_RIte : 'd ->
  ('j, 'k) GenGoal.fml ->
  ('j, 'k) GenGoal.exp ->
  ('j, 'k) GenGoal.exp ->
  'l ->
  'n ->
  'n ->
  'o

method virtual build_RLone : 'd -> 'a1

method virtual build_RNEq : 'd -> 'z

method virtual build_RNo : 'd -> 'a1

method virtual build_ROne : 'd -> 'a1

method virtual build_RProj : 'd -> 'r -> 's -> 't

method virtual build_RSome : 'd -> 'a1

method virtual build_RTClos : 'd -> 'b1

method virtual build_RUn : 'd ->
  GenGoal.runop ->
  ('j, 'k) GenGoal.exp ->
  'b1 ->
  'n ->
  'o

method virtual build_S : 'd -> 'i

method virtual build_Run : 'd -> ('j, 'k) GenGoal.block -> 'l list -> 'c1

method virtual build_Some_ : 'd -> 'h

method virtual build_Sub : 'd -> 'g

method virtual build_TClos : 'd -> 'b1

method virtual build_Transpose : 'd -> 'b1

method virtual build_True : 'd -> 'm

method virtual build_U : 'd -> 'i

method virtual build_Union : 'd -> 'r -> 's -> 't

method virtual build_Univ : 'd -> 'o

method virtual build_X : 'd -> 'u

method virtual build_exp : 'd ->
  ('j, 'k) GenGoal.exp ->
  'o ->
  Location.t ->
  int option ->
  'n

method virtual build_fml : 'd -> ('j, 'k) GenGoal.fml -> 'm -> Location.t -> 'l

method virtual build_iexp : 'd ->
  ('j, 'k) GenGoal.iexp ->
  'p ->
  Location.t ->
  'w

method virtual visit_'i : 'd -> 'k -> 'y

method virtual visit_'v : 'd -> 'j -> 'q

method visit_Run : 'd -> ('j, 'k) GenGoal.block -> 'c1

method visit_t : 'd -> ('j, 'k) GenGoal.t -> 'c1

method visit_fml : 'd -> ('j, 'k) GenGoal.fml -> 'l

method visit_True : 'd -> 'm

method visit_False : 'd -> 'm

method visit_Qual : 'd -> GenGoal.rqualify -> ('j, 'k) GenGoal.exp -> 'm

method visit_RComp : 'd ->
  ('j, 'k) GenGoal.exp ->
  GenGoal.comp_op ->
  ('j, 'k) GenGoal.exp ->
  'm

method visit_IComp : 'd ->
  ('j, 'k) GenGoal.iexp ->
  GenGoal.icomp_op ->
  ('j, 'k) GenGoal.iexp ->
  'm

method visit_LUn : 'd -> GenGoal.lunop -> ('j, 'k) GenGoal.fml -> 'm

method visit_LBin : 'd ->
  ('j, 'k) GenGoal.fml ->
  GenGoal.lbinop ->
  ('j, 'k) GenGoal.fml ->
  'm

method visit_Quant : 'd ->
  GenGoal.quant ->
  ('j, 'k) GenGoal.sim_binding list ->
  ('j, 'k) GenGoal.block ->
  'm

method visit_Let : 'd ->
  ('j, 'k) GenGoal.binding list ->
  ('j, 'k) GenGoal.block ->
  'm

method visit_FIte : 'd ->
  ('j, 'k) GenGoal.fml ->
  ('j, 'k) GenGoal.fml ->
  ('j, 'k) GenGoal.fml ->
  'm

method visit_Block : 'd -> ('j, 'k) GenGoal.block -> 'm

method visit_prim_fml : 'd -> ('j, 'k) GenGoal.prim_fml -> 'm

method visit_binding : 'd -> ('j, 'k) GenGoal.binding -> 'q * 'n

method visit_sim_binding : 'd ->
  ('j, 'k) GenGoal.sim_binding ->
  GenGoal.disj * 'q list * 'n

method visit_disj : 'd -> GenGoal.disj -> GenGoal.disj

method visit_block : 'd -> ('j, 'k) GenGoal.block -> 'l list

method visit_All : 'd -> 'h

method visit_Some_ : 'd -> 'h

method visit_No : 'd -> 'h

method visit_One : 'd -> 'h

method visit_Lone : 'd -> 'h

method visit_quant : 'd -> GenGoal.quant -> 'h

method visit_And : 'd -> 'i

method visit_Or : 'd -> 'i

method visit_Imp : 'd -> 'i

method visit_Iff : 'd -> 'i

method visit_U : 'd -> 'i

method visit_R : 'd -> 'i

method visit_S : 'd -> 'i

method visit_lbinop : 'd -> GenGoal.lbinop -> 'i

method visit_F : 'd -> 'u

method visit_G : 'd -> 'u

method visit_Not : 'd -> 'u

method visit_O : 'd -> 'u

method visit_X : 'd -> 'u

method visit_H : 'd -> 'u

method visit_P : 'd -> 'u

method visit_lunop : 'd -> GenGoal.lunop -> 'u

method visit_In : 'd -> 'z

method visit_NotIn : 'd -> 'z

method visit_REq : 'd -> 'z

method visit_RNEq : 'd -> 'z

method visit_comp_op : 'd -> GenGoal.comp_op -> 'z

method visit_IEq : 'd -> 'v

method visit_INEq : 'd -> 'v

method visit_Lt : 'd -> 'v

method visit_Lte : 'd -> 'v

method visit_Gt : 'd -> 'v

method visit_Gte : 'd -> 'v

method visit_icomp_op : 'd -> GenGoal.icomp_op -> 'v

method visit_exp : 'd -> ('j, 'k) GenGoal.exp -> 'n

method visit_None_ : 'd -> 'o

method visit_Univ : 'd -> 'o

method visit_Iden : 'd -> 'o

method visit_Ident : 'd -> 'k -> 'o

method visit_RUn : 'd -> GenGoal.runop -> ('j, 'k) GenGoal.exp -> 'o

method visit_RBin : 'd ->
  ('j, 'k) GenGoal.exp ->
  GenGoal.rbinop ->
  ('j, 'k) GenGoal.exp ->
  'o

method visit_RIte : 'd ->
  ('j, 'k) GenGoal.fml ->
  ('j, 'k) GenGoal.exp ->
  ('j, 'k) GenGoal.exp ->
  'o

method visit_BoxJoin : 'd ->
  ('j, 'k) GenGoal.exp ->
  ('j, 'k) GenGoal.exp list ->
  'o

method visit_Compr : 'd ->
  ('j, 'k) GenGoal.sim_binding list ->
  ('j, 'k) GenGoal.block ->
  'o

method visit_Prime : 'd -> ('j, 'k) GenGoal.exp -> 'o

method visit_prim_exp : 'd -> ('j, 'k) GenGoal.prim_exp -> 'o

method visit_ROne : 'd -> 'a1

method visit_RLone : 'd -> 'a1

method visit_RSome : 'd -> 'a1

method visit_RNo : 'd -> 'a1

method visit_rqualify : 'd -> GenGoal.rqualify -> 'a1

method visit_Transpose : 'd -> 'b1

method visit_TClos : 'd -> 'b1

method visit_RTClos : 'd -> 'b1

method visit_runop : 'd -> GenGoal.runop -> 'b1

method visit_Union : 'd -> 'r -> 's -> 't

method visit_Inter : 'd -> 'r -> 's -> 't

method visit_Over : 'd -> 'r -> 's -> 't

method visit_LProj : 'd -> 'r -> 's -> 't

method visit_RProj : 'd -> 'r -> 's -> 't

method visit_Prod : 'd -> 'r -> 's -> 't

method visit_Diff : 'd -> 'r -> 's -> 't

method visit_Join : 'd -> 'r -> 's -> 't

method visit_rbinop : 'd -> GenGoal.rbinop -> 'r -> 's -> 't

method visit_iexp : 'd -> ('j, 'k) GenGoal.iexp -> 'w

method visit_Num : 'd -> int -> 'p

method visit_Card : 'd -> ('j, 'k) GenGoal.exp -> 'p

method visit_IUn : 'd -> GenGoal.iunop -> ('j, 'k) GenGoal.iexp -> 'p

method visit_IBin : 'd ->
  ('j, 'k) GenGoal.iexp ->
  GenGoal.ibinop ->
  ('j, 'k) GenGoal.iexp ->
  'p

method visit_prim_iexp : 'd -> ('j, 'k) GenGoal.prim_iexp -> 'p

method visit_Neg : 'd -> 'x

method visit_iunop : 'd -> GenGoal.iunop -> 'x

method visit_Add : 'd -> 'g

method visit_Sub : 'd -> 'g

method visit_ibinop : 'd -> GenGoal.ibinop -> 'g

package electrod