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:
- specialized = true
- 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