mathlib documentation

core.init.meta.ac_tactics

source
meta constant tactic.flat_assoc (a a_1 a_2 : expr) :
tactic (expr × expr)

source
meta constant tactic.perm_ac (a a_1 a_2 a_3 a_4 : expr) :
tactic expr