max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/meta/interactive): typo

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-30 09:04:27 -08:00
parent 85b98f08e9
commit cc6d4a6ef8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/interactive.lean
View file

@ -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 :=