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

fix(reflect): change names

Browse source
This commit is contained in:
Rob Lewis 2017-06-07 17:22:11 -04:00 • committed by Sebastian Ullrich
parent 0e0070eb2f
commit b8e5de2fb7
2 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -49,9 +49,8 @@ meta instance prod.reflect {α β : Type} [has_reflect α] [reflected α] [has_r
meta instance pos.reflect : has_reflect pos
| ⟨l, c⟩ := `(_)
meta def reflect_to_format {α} {a : α} (h : reflected a) : format :=
meta def reflected.to_format {α} {a : α} (h : reflected a) : format :=
to_fmt (reflect a).to_expr
meta instance reflected.has_to_format {α} (a : α) : has_to_format (reflected a) :=
⟨reflect_to_format⟩
meta instance {α} (a : α) : has_to_format (reflected a) :=
⟨reflected.to_format⟩

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

@ -189,11 +189,11 @@ meta def option_to_tactic_format {α : Type u} [has_to_tactic_format α] : optio
meta instance {α : Type u} [has_to_tactic_format α] : has_to_tactic_format (option α) :=
⟨option_to_tactic_format⟩
meta def reflect_to_tactic_format {α} {a : α} (h : reflected a) : tactic format :=
meta def reflected.to_tactic_format {α} {a : α} (h : reflected a) : tactic format :=
pp (reflect a).to_expr
meta instance reflected.has_to_tactic_format {α} (a : α) : has_to_tactic_format (reflected a) :=
⟨reflect_to_tactic_format⟩
meta instance {α} (a : α) : has_to_tactic_format (reflected a) :=
⟨reflected.to_tactic_format⟩
@[priority 10] meta instance has_to_format_to_has_to_tactic_format (α : Type) [has_to_format α] : has_to_tactic_format α :=
⟨(λ x, return x) ∘ to_fmt⟩