mathlib documentation

core.init.control.applicative

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

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

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

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

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

Instances