Documentation

Make fresh, hygienic names for every parameter and index of an inductive declaration.

For example, inductive Foo {α : Type} : Nat → Type will give something like #[`α✝, `a✝].

Return the inductive declaration's type applied to the arguments in argNames.

Return implicit binder syntaxes for the given argNames. The output matches implicitBinder*.

For example, #[`foo,`bar] gives `({foo} {bar}).

Return instance binder syntaxes binding className α for every generic parameter α of the inductive indVal for which such a binding is type-correct. argNames is expected to provide names for the parameters (see mkInductArgNames). The output matches instBinder*.

For example, given inductive Foo {α : Type} (n : Nat) : (β : Type) → Type, where β is an index, invoking mkInstImplicitBinders `BarClass foo #[`α, `n, `β] gives `([BarClass α]).