mathlib documentation

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

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}]]