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

refactor(init/meta): drop obsolete X.to_expr functions

Browse source
This commit is contained in:
Sebastian Ullrich 2017-02-21 00:55:37 +01:00 • committed by Leonardo de Moura
parent a053175714
commit 69741061b0
3 changed files with 5 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/meta/quote.lean
View file

@ -48,9 +48,3 @@ meta instance : has_quote unit := ⟨λ _, ``(unit.star)⟩
meta instance {α β : Type} [has_quote α] [has_quote β] : has_quote (α × β) :=
⟨λ ⟨x, y⟩, ``((%%(quote x), %%(quote y)))⟩
meta def nat.to_expr : nat → tactic expr := λ n, to_expr $ quote n
meta def char.to_expr : char → tactic expr := λ n, to_expr $ quote n
meta def unsigned.to_expr : unsigned → tactic expr := λ n, to_expr $ quote n
meta def name.to_expr : name → tactic expr := λ n, to_expr $ quote n
meta def list_name.to_expr : list name → tactic expr := λ n, to_expr $ quote n

3
library/init/meta/simp_tactic.lean
View file

@ -373,8 +373,7 @@ meta def to_simp_lemmas : simp_lemmas → list name → tactic simp_lemmas
meta def mk_simp_attr (attr_name : name) : command :=
do t ← to_expr ``(caching_user_attribute simp_lemmas),
a ← attr_name^.to_expr,
v ← to_expr ``({name := %%a,
v ← to_expr ``({name := %%(quote attr_name),
descr := "simplifier attribute",
mk_cache := λ ns, do {tactic.to_simp_lemmas simp_lemmas.mk ns},
dependencies := [`reducibility] } : caching_user_attribute simp_lemmas),

10
library/init/meta/smt/ematch.lean
View file

@ -79,9 +79,8 @@ meta def to_hinst_lemmas_core (m : transparency) : bool → list name → hinst_
meta def mk_hinst_lemma_attr_core (attr_name : name) (as_simp : bool) : command :=
do t ← to_expr ``(caching_user_attribute hinst_lemmas),
a ← attr_name^.to_expr,
b ← if as_simp then to_expr ``(tt) else to_expr ``(ff),
v ← to_expr ``({name := %%a,
v ← to_expr ``({name := %%(quote attr_name),
descr := "hinst_lemma attribute",
mk_cache := λ ns, to_hinst_lemmas_core reducible %%b ns hinst_lemmas.mk,
dependencies := [`reducibility] } : caching_user_attribute hinst_lemmas),
@ -117,10 +116,9 @@ meta def mk_hinst_lemma_attr_set (attr_name : name) (attr_names : list name) (si
do mk_hinst_lemma_attrs_core ff attr_names,
mk_hinst_lemma_attrs_core tt simp_attr_names,
t ← to_expr ``(caching_user_attribute hinst_lemmas),
a ← attr_name^.to_expr,
l1 ← list_name.to_expr attr_names,
l2 ← list_name.to_expr simp_attr_names,
v ← to_expr ``({name := %%a,
l1 ← return $ quote attr_names,
l2 ← return $ quote simp_attr_names,
v ← to_expr ``({name := %%(quote attr_name),
descr := "hinst_lemma attribute set",
mk_cache := λ ns,
let aux1 : list name := %%l1,