scilib documentation

core / init.control.applicative

source
@[class]
structure has_pure (f : Type u → Type v) :
Type (max (u+1) v)
  • pure : Π {α : Type ?}, α → f α
Instances of this typeclass
Instances of other typeclasses for has_pure
  • has_pure.has_sizeof_inst
source
@[class]
structure has_seq (f : Type u → Type v) :
Type (max (u+1) v)
  • seq : Π {α β : Type ?}, f (α → β) → f α → f β
Instances of this typeclass
Instances of other typeclasses for has_seq
  • has_seq.has_sizeof_inst
source
@[class]
structure has_seq_left (f : Type u → Type v) :
Type (max (u+1) v)
  • seq_left : Π {α β : Type ?}, f α → f β → f α
Instances of this typeclass
Instances of other typeclasses for has_seq_left
  • has_seq_left.has_sizeof_inst
source
@[class]
structure has_seq_right (f : Type u → Type v) :
Type (max (u+1) v)
  • seq_right : Π {α β : Type ?}, f α → f β → f β
Instances of this typeclass
Instances of other typeclasses for has_seq_right
  • has_seq_right.has_sizeof_inst
source
@[class]
structure applicative (f : Type u → Type v) :
Type (max (u+1) v)
Instances of this typeclass
Instances of other typeclasses for applicative
  • applicative.has_sizeof_inst