Consider a type ψ which is an inductive datatype using a single constructor mk (a : α) (b : β) : ψ.
Lean will automatically make two projection functions a : ψ → α, b : ψ → β.
Lean tags these declarations as projections.
This helps the simplifier / rewriter not have to expand projectors.
Eg a (mk x y) will automatically reduce to x.
If you extend a structure, all of the projections on the parent will also be created for the child.
Projections are also treated differently in the VM for efficiency.
Note that projections have nothing to do with the dot mylist.map syntax.
Add a new general inductive declaration to the environment.
This has the same effect as a inductive in the file, including generating
all the auxiliary definitions, as well as triggering mutual/nested inductive
compilation, by contrast to environment.add_inductive which only adds the
core axioms supported by the kernel.
The inds argument should be a list of inductives in the mutual family.
The first argument is a pair of the name of the type being constructed
and the type of this inductive family (not including the params).
The second argument is a list of intro rules, specified by a name, an
implicit_infer_kind giving the implicitness of the params for this constructor,
and an expression with the type of the constructor (not including the params).
Technically, this works by checking if the name is in the ginductive environment
extension which is outside the kernel, whereas is_inductive works by looking at the kernel extension.
But there are no is_inductives which are not is_ginductive.