What is `abbreviation`?

Stream: general

[Scott Morrison]

In particular, what is the difference between using abbreviation and using @[reducible] def? I remember being told that it's the most transparent setting of all, but I don't know of any documentation of this.

[Mario Carneiro]

it combines reducible with a kernel reducibility setting IIRC

[Mario Carneiro]

You used to have to use some tactic hackery to write a def with this semantics, and there was only one example, id_rhs. I always viewed it as an internal thing, but then it got its own keyword. I don't know why, perhaps @Sebastian Ullrich knows?

[Mario Carneiro]

The most transparent setting of all is of course notation

[Johan Commelin]

Is notation also a def?

[Mario Carneiro]

no

[Johan Commelin]

Aah, ok

[Johan Commelin]

I would have been very surprised.

[Sebastian Ullrich]

There is no transparency difference between abbreviation and @[reducible] def, it's just a performance hint. I like using abbreviation when I want to signify that this definition really is immaterial (basically a notation but with namespacing), but in practice the difference between the two shouldn't matter.