[Merged by Bors] - feat(meta/univs): Add a reflect_name tactic, make reflected instances universe polymorphic #14766
Conversation
…es universe polymorphic
eric-wieser
added
awaiting-review
| ⟨level.succ reflect_univ.{u}⟩ | ||
|
|
||
| @[instance] meta def {u v} reflect_univ.max [reflected_univ.{u}] [reflected_univ.{v}] : | ||
| reflected_univ.{max u v} := |
There was a problem hiding this comment.
I'm (happily) surprised that this works. I would have expected this to be a blanket instance, with Lean reasoning that u = max u u or u = max u 0.
| do | ||
| tgt ← tactic.target, | ||
| `(reflected %%x) ← pure tgt, | ||
| expr.const name levels ← pure x, |
There was a problem hiding this comment.
It would be fairly straightforward to extend this tactic to applications as well and try apply_instance first, and then you don't need write the subst manually.
But I really don't want to encourage you to spend too much time on Lean 3 metaprogramming.
There was a problem hiding this comment.
I don't think trying apply_instance first is a good idea; as seen in the thread that started this, it can end up synthesizing an instance that doesn't type-check.
But I really don't want to encourage you to spend too much time on Lean 3 metaprogramming.
I think probably I'd rather leave this as is; it's all a rabbit hole that appeared while trying to refactor #14665, and this particular PR wasn't even needed by that refactor!
| ((by reflect_name : reflected @vector.nil.{u}).subst `(α)) | ||
| (λ n x xs ih, (by reflect_name : reflected @vector.cons.{u}).subst₄ `(α) `(n) `(x) ih) |
There was a problem hiding this comment.
| ((by reflect_name : reflected @vector.nil.{u}).subst `(α)) | |
| (λ n x xs ih, (by reflect_name : reflected @vector.cons.{u}).subst₄ `(α) `(n) `(x) ih) | |
| (by resetI; reflect) | |
| (λ n x xs ih, by resetI; reflect) |
This is how it could look like if you extended reflect_name to applications.
github-actions
bot
removed
the
awaiting-CI
|
bors r+ |
github-actions
bot
added
ready-to-merge
… universe polymorphic (#14766) The existing `list.reflect` instance only works for `Type 0`, this version works for `Type u` providing `u` is known.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
The existing
list.reflectinstance only works forType 0, this version works forType uprovidinguis known.