DefinitionsAssocRel, FreeAddSemigroup, instAddSemigroup, instInhabited, map, of, FreeAddMagma, instAdd, instInhabited, instMonad, instTraversable, length, liftAux, map, recOnAdd, recOnPure, repr, toFreeAddSemigroup, traverse, FreeAddMagmaAssocQuotientEquiv, FreeAddSemigroup, head, instAddSemigroup, instDecidableEq, instInhabited, instMonad, instTraversable, length, map, of, recOnAdd, recOnPure, tail, traverse, FreeMagma, instInhabited, instMonad, instMul, instTraversable, length, liftAux, map, recOnMul, recOnPure, repr, toFreeSemigroup, traverse, FreeMagmaAssocQuotientEquiv, FreeSemigroup, head, instDecidableEq, instInhabited, instMonad, instSemigroup, instTraversable, length, map, of, recOnMul, recOnPure, tail, traverse, AssocQuotient, instInhabited, instSemigroup, map, of, AssocRel, instDecidableEqFreeAddMagma, decEq, instDecidableEqFreeMagma, decEq, instReprFreeAddMagma, instReprFreeMagma | 74 |
Theoremshom_ext, hom_ext_iff, induction_on, lift_comp_of, lift_comp_of', lift_of, lift_symm_apply, map_of, quot_mk_assoc, quot_mk_assoc_left, add_bind, add_eq, add_seq, hom_ext, hom_ext_iff, instLawfulMonad, instLawfulTraversable, length_pos, length_toFreeAddSemigroup, lift_comp_of, lift_comp_of', lift_of, lift_symm_apply, map_add', map_of, map_pure, pure_bind, pure_seq, toFreeAddSemigroup_comp_map, toFreeAddSemigroup_comp_of, toFreeAddSemigroup_map, toFreeAddSemigroup_of, traverse_add, traverse_add', traverse_eq, traverse_pure, traverse_pure', add_bind, add_seq, ext, ext_iff, head_add, hom_ext, hom_ext_iff, instLawfulMonad, instLawfulTraversable, length_add, length_map, length_of, lift_comp_of, lift_comp_of', lift_of, lift_of_add, lift_symm_apply, map_add', map_of, map_pure, mk_add_mk, of_head, of_tail, pure_bind, pure_seq, tail_add, traverse_add, traverse_add', traverse_eq, traverse_pure, traverse_pure', hom_ext, hom_ext_iff, instLawfulMonad, instLawfulTraversable, length_pos, length_toFreeSemigroup, lift_comp_of, lift_comp_of', lift_of, lift_symm_apply, map_mul', map_of, map_pure, mul_bind, mul_eq, mul_seq, pure_bind, pure_seq, toFreeSemigroup_comp_map, toFreeSemigroup_comp_of, toFreeSemigroup_map, toFreeSemigroup_of, traverse_eq, traverse_mul, traverse_mul', traverse_pure, traverse_pure', ext, ext_iff, head_mul, hom_ext, hom_ext_iff, instLawfulMonad, instLawfulTraversable, length_map, length_mul, length_of, lift_comp_of, lift_comp_of', lift_of, lift_of_mul, lift_symm_apply, map_mul', map_of, map_pure, mk_mul_mk, mul_bind, mul_seq, of_head, of_tail, pure_bind, pure_seq, tail_mul, traverse_eq, traverse_mul, traverse_mul', traverse_pure, traverse_pure', hom_ext, hom_ext_iff, induction_on, lift_comp_of, lift_comp_of', lift_of, lift_symm_apply, map_of, quot_mk_assoc, quot_mk_assoc_left | 136 |