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

fix(library/init/meta/simp_tactic): typo

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-04 19:51:12 -07:00
parent 76fca40be2
commit e2de6ab28b
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/simp_tactic.lean
View file

@ -115,7 +115,7 @@ do t ← to_expr `(caching_user_attribute simp_lemmas),
v ← to_expr `(({ name := %%a,
descr := "simplifier attribute",
mk_cache := λ ns, do {tactic.to_simp_lemmas simp_lemmas.mk ns},
dependencies := [`reducible] } : caching_user_attribute simp_lemmas)),
dependencies := [`reducibility] } : caching_user_attribute simp_lemmas)),
add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
attribute.register attr_name