mathlib
f05c49f6
- feat(meta/univs): Add a reflect_name tactic, make reflected instances universe polymorphic (#14766)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(meta/univs): Add a reflect_name tactic, make reflected instances universe polymorphic (#14766) The existing `list.reflect` instance only works for `Type 0`, this version works for `Type u` providing `u` is known.
Author
eric-wieser
Parents
8187142b
Loading