mathlib3 documentation

• pure : Π {α : Type ?}, α → f α

Instances of this typeclass

• applicative.to_has_pure
• functor.comp.has_pure
• filter.has_pure
• ultrafilter.has_pure
• finset.has_pure

Instances of other typeclasses for has_pure

• has_pure.has_sizeof_inst

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

Instances of this typeclass

• applicative.to_has_seq
• functor.comp.has_seq
• filter.has_seq

Instances of other typeclasses for has_seq

• has_seq.has_sizeof_inst

• seq_left : Π {α β : Type ?}, f α → f β → f α

Instances of this typeclass

• applicative.to_has_seq_left

Instances of other typeclasses for has_seq_left

• has_seq_left.has_sizeof_inst

• seq_right : Π {α β : Type ?}, f α → f β → f β

Instances of this typeclass

• applicative.to_has_seq_right

Instances of other typeclasses for has_seq_right

• has_seq_right.has_sizeof_inst

• to_functor : functor f
• to_has_pure : has_pure f
• to_has_seq : has_seq f
• to_has_seq_left : has_seq_left f
• to_has_seq_right : has_seq_right f

Instances of this typeclass

• alternative.to_applicative
• monad.to_applicative
• functor.comp.applicative
• functor.const.applicative
• functor.add_const.applicative
• filter.applicative
• finset.applicative

Instances of other typeclasses for applicative

• applicative.has_sizeof_inst