mathlib documentation

core.init.meta.fun_info

structure param_info  :
Type

structure fun_info  :
Type

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

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.

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

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