What is the difference between `abbrev` and `@[inline] def`?

Stream: lean4

[Victor Porton]

What is the difference between abbrev and @[inline] def?

[Robin Arnez]

Well, abbrev is @[inline, reducible] def (+ some change to defeq), so it doesn't only affect compilation but also e.g. instance search or tactics like simp which will be able to look through the abbrev. Example:

def MyNat := Nat
#check (0 : MyNat) -- fails

@[inline] def MyNat2 := Nat
#check (0 : MyNat2) -- fails

abbrev MyNat3 := Nat
#check (0 : MyNat3) -- succeeds

[Jovan Gerbscheid]

Since the module system there is also another difference. abbrev now also adds the @[expose] tag.