mathlib documentation

core / init.meta.fun_info

structure param_info  :
Type
@[protected, instance]
structure fun_info  :
Type
@[protected, 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

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} (f : α → exprtactic α) :
list exprlist param_infoα → tactic α
meta def tactic.fold_explicit_args {α : Type} (e : expr) (a : α) (f : α → exprtactic α) :