mathlib documentation

core.init.meta.ac_tactics

meta constant tactic.flat_assoc  :
exprexprexprtactic (expr × expr)

meta constant tactic.perm_ac  :
exprexprexprexprexprtactic expr