mathlib3 documentation

• map : Π {α β : Type ?}, (α → β) → f α → f β
• map_const : Π {α β : Type ?}, α → f β → f α

Instances of this typeclass

• bifunctor.functor
• applicative.to_functor
• traversable.to_functor
• tagged_format.is_functor
• widget.attr.is_functor
• widget.html.is_functor
• functor.const.functor
• functor.add_const.functor
• functor.comp.functor
• tactic.interactive.ac_mono_ctx'.functor
• filter.functor
• ultrafilter.functor
• measure_theory.outer_measure.functor
• slim_check.tree.functor
• slim_check.small.functor
• slim_check.large.functor
• witt_vector.functor
• stream.seq.functor
• pfunctor.obj.functor
• multiset.functor
• finset.functor

Instances of other typeclasses for functor

• functor.has_sizeof_inst