mathlib documentation

core.init.control.applicative

@[class]
structure has_pure  :
(Type uType v)Type (max (u+1) v)
  • pure : Π {α : Type ?}, α → f α

Instances
@[class]
structure has_seq  :
(Type uType v)Type (max (u+1) v)
  • seq : Π {α β : Type ?}, f (α → β)f αf β

Instances
@[class]
structure has_seq_left  :
(Type uType v)Type (max (u+1) v)
  • seq_left : Π {α β : Type ?}, f αf βf α

Instances
@[class]
structure has_seq_right  :
(Type uType v)Type (max (u+1) v)
  • seq_right : Π {α β : Type ?}, f αf βf β

Instances
@[class]
structure applicative  :
(Type uType v)Type (max (u+1) v)

Instances