mathlib3
c45e5d58 - fix(meta/expr): remove `has_reflect.has_to_pexpr` (#14901)

Commit
3 years ago
fix(meta/expr): remove `has_reflect.has_to_pexpr` (#14901) This instance (introduced in #3477) forms a diamond with the builtin `pexpr.has_to_pexpr`: ```lean import meta.expr #eval show tactic unit, from do let i1 : has_to_pexpr pexpr := pexpr.has_to_pexpr, let i2 : has_to_pexpr pexpr := has_reflect.has_to_pexpr, let e := ``(1), let p1 := @to_pexpr _ i1 e, let p2 := @to_pexpr _ i2 e, guard (p1 = p2) -- fails ``` The consequence is that in cases where `bar` is not a `pexpr` or `expr` but a value to be reflected, ``` ``(foo %%bar) ``` now has to be written ``` ``(foo %%`(bar)) ```; a spelling already used in various existing files. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Instance.20diamonds.20in.20has_to_pexpr/near/287083928)
Author
Parents
Loading