# mathlibdocumentation

core / init.meta.fun_info

structure param_info  :
Type
• is_implicit : bool
• is_inst_implicit : bool
• is_prop : bool
• has_fwd_deps : bool
• back_deps :
@[instance]
structure fun_info  :
Type
• params :
• result_deps :
meta def fun_info_to_format  :
@[instance]
structure subsingleton_info  :
Type
• specialized : bool
• is_subsingleton : bool

specialized is true if the result of fun_info has been specifialized using this argument. For example, consider the function

       f : Pi (α : Type), α -> α


Now, suppse we request get_specialize fun_info for the application

   f unit a


fun_info_manager returns two param_info objects:

1. specialized = true
2. is_subsingleton = true

Note that, in general, the second argument of f is not a subsingleton, but it is in this particular case/specialization.

\remark This bit is only set if it is a dependent parameter.

Moreover, we only set is_specialized IF another parameter becomes a subsingleton

@[instance]
meta constant tactic.get_fun_info (f : expr) (nargs : := none)  :

If nargs is not none, then return information assuming the function has only nargs arguments.

meta constant tactic.get_subsingleton_info (f : expr) (nargs : := none)  :
meta constant tactic.get_spec_subsingleton_info (t : expr)  :

get_spec_subsingleton_info t return subsingleton parameter information for the function application t of the form f a_1 ... a_n.

This tactic is more precise than get_subsingleton_info f and get_subsingleton_info_n f n

Example: given f : Pi (α : Type), α -> α, get_spec_subsingleton_info for

f unit b

returns a fun_info with two param_info

1. specialized = tt
2. is_subsingleton = tt

The second argument is marked as subsingleton only because the resulting information is taking into account the first argument.

meta constant tactic.get_spec_prefix_size (t : expr) (nargs : )  :
meta def tactic.fold_explicit_args_aux {α : Type u_1} (f : α → expr) :
α →
meta def tactic.fold_explicit_args {α : Type} (e : expr) (a : α) (f : α → expr) :