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

feat(init/meta/pexpr): has_to_pexpr (reflected a)

Browse source
This commit is contained in:
Sebastian Ullrich 2017-05-30 16:48:31 +02:00 • committed by Leonardo de Moura
parent 77264a6074
commit 59184e888f
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/init/meta/pexpr.lean
View file

@ -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⟩