diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index ff32fdb1d7..7f1dfd7896 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -391,7 +391,7 @@ tactic.symmetry meta def transitivity : tactic unit := tactic.transitivity -meta def ac_reflixivity : tactic unit := +meta def ac_reflexivity : tactic unit := tactic.ac_refl meta def ac_refl : tactic unit :=