mathlib documentation

core / init.meta.fun_info

source
structure param_info  :
Type
source
meta def param_info.to_format  :
param_info → format
source
@[protected, instance]
meta def param_info.has_to_format  :
has_to_format param_info
source
structure fun_info  :
Type
source
meta def fun_info_to_format  :
fun_info → format
source
@[protected, instance]
meta def fun_info.has_to_format  :
has_to_format fun_info
source
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

source
meta def subsingleton_info_to_format  :
subsingleton_info → format
source
@[protected, instance]
meta def subsingleton_info.has_to_format  :
has_to_format subsingleton_info
source
meta constant tactic.get_fun_info (f : expr) (nargs : option ℕ := none) (md : tactic.transparency := semireducible) :
tactic fun_info

If nargs is not none, then return information assuming the function has only nargs arguments.

source
meta constant tactic.get_subsingleton_info (f : expr) (nargs : option ℕ := none) (md : tactic.transparency := semireducible) :
tactic (list subsingleton_info)
source
meta constant tactic.get_spec_subsingleton_info (t : expr) (md : tactic.transparency := semireducible) :
tactic (list subsingleton_info)

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.

source
meta constant tactic.get_spec_prefix_size (t : expr) (nargs : ℕ) (md : tactic.transparency := semireducible) :
tactic ℕ
source
meta def tactic.fold_explicit_args_aux {α : Type u_1} (f : α → expr → tactic α) :
list expr → list param_info → α → tactic α
source
meta def tactic.fold_explicit_args {α : Type} (e : expr) (a : α) (f : α → expr → tactic α) :
tactic α