when to use abbrev over def?

Stream: general

[Lhr]

given

def positive n := n > 0
def negative n := n < 0

which is the better way to define neutral?

def neutral n := ¬(positive n ∨ negative n)
abbrev neutral n := ¬(positive n ∨ negative n)

This is a toy example, I run into this question often

[Henrik Böving]

When you want type class instances of the thing on the rhs of your def to be reused for the thing you are defining use abbrev, otherwise don't.

[Mirek Olšák]

I don't think it is only about typeclass instances. Also simp can often see through abbrev, and you might not want to create a new set of simp lemmas just for a thin layer above.

[Shreyas Srinivas]

Henrik Böving said:

When you want type class instances of the thing on the rhs of your def to be reused for the thing you are defining use abbrev, otherwise don't.

Or when you are defining a type and don’t want to have to tell lean that the lhs and rhs are equal by definition when a type check fails