Jason Gross (Mar 12 2021 at 14:51):
Is there a way to declare that certain constants should be unfoldable during typeclass instance search?
Leonardo de Moura (Mar 13 2021 at 04:11):
You can mark declarations with the
Leonardo de Moura (Mar 13 2021 at 04:12):
abbrev f ... is sugar for
@[reducible, inline] def f ...
Last updated: May 07 2021 at 12:15 UTC