abbrev vs reducible

Stream: lean4

[Horatiu Cheval]

Is there any difference between abbrev and @[reducible] def? I found them interchangeable in my usage so far.

[Leonardo de Moura]

abbrev also includes the [inline] attribute and a hint to the kernel. [reducible] is a hint to the elaborator, and the kernel doesn't even know it exists.