Structures · Lean core
Std.Associative
Associative op indicates op is an associative operation,
i.e. (a ∘ b) ∘ c = a ∘ (b ∘ c).
- Defined in
- Init.Core
- Shape
- One type argument · adds assoc
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances22
- Int
- Nat
- Rat
- Bool
- BitVec
- UInt64
- UInt8
- UInt16
- UInt32
- USize
- Int32
- Int8
- Int64
- Int16
- ISize
- String
- Ordering
- Fin
- List
- Set
- Finset
- Option
How is a type an instance?
Loading the hierarchy index…
Assumed by57
- Finset.fold
- Multiset.fold
- Multiset.fold_cons_left
- Finset.fold_insert
- Finset.fold_congr
- Multiset.fold_add
- Multiset.fold.congr_simp
- Finset.fold_cons
- Multiset.fold_zero
- Finset.fold_op_rel_iff_and
- Finset.fold_insert_idem
- Multiset.noncommFold
- Finset.fold_op_rel_iff_or
- Multiset.noncommFold_coe
- Multiset.fold_dedup_idem
- Finset.fold_ite
- Finset.fold_empty
- Finset.fold_image_idem
- Multiset.fold_cons'_right
- Finset.fold_disjSum
- Multiset.coe_fold_r
- Finset.fold_singleton
- Finset.fold_disjUnion
- Finset.fold_union_inter
- Finset.fold.congr_simp
- Finset.fold_op_distrib
- List.Perm.foldr_op_eq
- Finset.fold_disjiUnion
- Finset.fold_image
- Finset.fold_map
- Multiset.fold_singleton
- Multiset.fold_cons_right
- List.foldl1_eq_foldr1
- Multiset.coe_fold_l
- Multiset.fold_bind
- Multiset.fold_hom
- Multiset.fold_eq_foldl
- Finset.fold_ite'
- Finset.fold_const
- List.foldl_eq_foldr_of_commute
- Multiset.fold_distrib
- Multiset.noncommFold_empty
- Multiset.fold_cons'_left
- List.foldl_op_eq_op_foldr_assoc
- Equiv.instAssociativeCoeForallForallArrowCongr
- Multiset.noncommFold.congr_simp
- Multiset.noncommFold_eq_fold
- Multiset.fold_eq_foldr
- Multiset.fold_union_inter
- Finset.fold_hom
Ancestors0
No ancestors.