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

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

Browse source
This commit is contained in:
Jeremy Avigad 2016-08-18 10:12:59 -07:00 • committed by Leonardo de Moura
parent 440d30300f
commit 4af0e0a2de
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

@ -17,7 +17,7 @@ meta_constant simp_lemmas : Type₁
computed with respect to the given transparency setting. -/
meta_constant mk_simp_lemmas_core : transparency → list name → list name → tactic simp_lemmas
/- Create an empty simp_lemmas. That is, it ignores the lemmas marked with the [simp] attribute. -/
meta_constant mk_empy_simp_lemmas : tactic simp_lemmas
meta_constant mk_empty_simp_lemmas : tactic simp_lemmas
/- (simp_lemmas_insert_core m lemmas id lemma priority) adds the given lemma to the set simp_lemmas. -/
meta_constant simp_lemmas_insert_core : transparency → simp_lemmas → expr → tactic simp_lemmas