mathlib3 documentation

core / init.control.applicative

@[class]
structure has_pure (f : Type u Type v) :
Type (max (u+1) v)
Instances of this typeclass
Instances of other typeclasses for has_pure
  • has_pure.has_sizeof_inst
@[class]
structure has_seq (f : Type u Type v) :
Type (max (u+1) v)
Instances of this typeclass
Instances of other typeclasses for has_seq
  • has_seq.has_sizeof_inst
@[class]
structure has_seq_left (f : Type u Type v) :
Type (max (u+1) v)
Instances of this typeclass
Instances of other typeclasses for has_seq_left
  • has_seq_left.has_sizeof_inst
@[class]
structure has_seq_right (f : Type u Type v) :
Type (max (u+1) v)
Instances of this typeclass
Instances of other typeclasses for has_seq_right
  • has_seq_right.has_sizeof_inst
@[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