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