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
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
f : Pi (α : Type), α -> α,
f unit b
returns a fun_info with two param_info
- specialized = tt
- is_subsingleton = tt
The second argument is marked as subsingleton only because the resulting information is taking into account the first argument.