mathlib3 documentation

core / init.meta.rec_util

meta def tactic.is_type_app_of (e : expr) (I_name : name) :

Return tt iff e's type is of the form (I_name ...)

meta def tactic.mk_brec_on_rec_value (F_name : name) (i : ) :

Construct brec_on "recursive value". F_name is the name of the brec_on "dictionary". Type of the F_name hypothesis should be of the form (below (C ...)) where C is a constructor. The result is the "recursive value" for the (i+1)-th recursive value of the constructor C.

Return a list of names of the form [p.i, ..., p.{i+n}] where n is the number of fields of the constructor c

Given an inductive datatype I with k constructors and where constructor i has n_i fields, return the list [[p.1, ..., p.n_1], [p.{n_1 + 1}, ..., p.{n_1 + n_2}], ..., [..., p.{n_1 + ... + n_k}]]