mathlib documentation

core / init.control.applicative

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

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

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

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

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

Instances