mathlib documentation

core / init.meta.ac_tactics

meta constant tactic.flat_assoc :

expr → expr → expr → tactic (expr × expr)

meta constant tactic.perm_ac :

expr → expr → expr → expr → expr → tactic expr