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
If nargs is not none, then return information assuming the function has only nargs arguments.
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.