Describe the error
The Lean Language Reference, Ch 14. type class : Functor
Given a : α and v : f α, mapConst a v is equivalent to Function.const _ a <$> v. For some functors, this can be implemented more efficiently; for all other functors, the default implementation may be used.
Here, I think that the type of v must be f $\beta$ ( or f _ )
The VScode Lean extensions also display same description, but if my understanding is correct, the second argument of Functor.mapConst must be the domain instance of constant function ( $f \beta \rightarrow f \alpha$ ) so the type of v must be f $\beta$.
Thank you,
Describe the error
The Lean Language Reference, Ch 14. type class : Functor
Here, I think that the type of v must be f$\beta$ ( or f _ )$f \beta \rightarrow f \alpha$ ) so the type of v must be f $\beta$ .
The VScode Lean extensions also display same description, but if my understanding is correct, the second argument of Functor.mapConst must be the domain instance of constant function (
Thank you,