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✝]
.
Equations
Instances For
Return the inductive declaration's type applied to the arguments in argNames
.
Equations
Instances For
def
Lean.Elab.Deriving.mkInstImplicitBinders
(className : Name)
(indVal : InductiveVal)
(argNames : Array Name)
:
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 α])
.
Equations
Instances For
- typeInfos : Array InductiveVal
- usePartial : Bool