# 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  :
expr

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

meta constant tactic.get_subsingleton_info  :
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  :
expr

meta def tactic.fold_explicit_args_aux {α : Type u_1} :
(α → exprtactic α)α →

meta def tactic.fold_explicit_args {α : Type} :
exprα → (α → exprtactic α)