Module `Imandra_surface.Count_funs`

Count functions, for types that need it

val mk_count_fun_ty : ?⁠db:Event.DB.t -> ?⁠find_cnt:(Uid.t -> Event.fun_data option) -> Type.t -> Event.fun_data: takes ty and builds a function ty -> int

val mk_count_fun_ty_as_lam : ?⁠db:Event.DB.t -> ?⁠find_cnt:(Uid.t -> Event.fun_data option) -> Type.t -> Term.t: Same as mk_count_fun_ty but returns a lambda term.

val mk_count_fun_tuple : ?⁠db:Event.DB.t -> ?⁠find_cnt:(Uid.t -> Event.fun_data option) -> Type.t list -> Event.fun_data: takes ty1…tyn and builds a function (ty1 * … * tyn) -> int

val mk_count_funs : ?⁠db:Event.DB.t -> ?⁠find_cnt:(Uid.t -> Event.fun_data option) -> Type.def list -> (Uid.t * Term.t * Event.fun_data) list: takes type definitions and returns the type name, a function term and function definition for each of the type def.