From 59184e888f75c9f205e7e68a09d09526ff9dc5eb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 30 May 2017 16:48:31 +0200 Subject: [PATCH] feat(init/meta/pexpr): has_to_pexpr (reflected a) --- library/init/meta/pexpr.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean index c369ab68c9..fa48989be5 100644 --- a/library/init/meta/pexpr.lean +++ b/library/init/meta/pexpr.lean @@ -18,10 +18,10 @@ meta constant pexpr.mk_explicit : pexpr → pexpr /- Choice macros are used to implement overloading. -/ meta constant pexpr.is_choice_macro : pexpr → bool -meta class has_to_pexpr (α : Type u) := +meta class has_to_pexpr (α : Sort u) := (to_pexpr : α → pexpr) -meta def to_pexpr {α : Type u} [has_to_pexpr α] : α → pexpr := +meta def to_pexpr {α : Sort u} [has_to_pexpr α] : α → pexpr := has_to_pexpr.to_pexpr meta instance : has_to_pexpr pexpr := @@ -29,3 +29,6 @@ meta instance : has_to_pexpr pexpr := meta instance : has_to_pexpr expr := ⟨pexpr.of_expr⟩ + +meta instance (α : Sort u) (a : α) : has_to_pexpr (reflected a) := +⟨pexpr.of_expr ∘ reflected.to_expr⟩