def vs abbrev

Stream: lean4

[Yuri de Wit]

It is not clear to me when should I use def vs abbrev?

abbrev PairCtx  := (Type × List (String × Type))
#check ((Nat, [("a", Int)]) : PairCtx)

vs

def    PairCtx2 := (Type × List (String × Type))
#check ((Nat, [("a", Int)]) : PairCtx2)

[Henrik Böving]

you can in fact always use def, abbrev is a shortcut for a def tagged with @[reducible] which has the very nice effect of allowing type class synthesis to look through your definition (it normally wouldnt do this)

This means if you are for example defining a custom monad stack and use abbrev it will automatically infer the Monad instance for this type while if you use def it won't.

[Mario Carneiro]

Reducible definitions should be avoided unless necessary, because lean will have to unfold these a lot, and if you have multiple layers of reducible definitions the terms that lean is working with can get really big really fast.

To your question, although they are actually definitions, so they will be represented as written as long as they are not unfolded, it is easy for unification or other operations to end up unfolding these definitions and so the underlying definition will show up. By comparison, if you use notation to define an abbreviation, it is really erased at parse time so there is no difference between it and the definition it abbreviates.

[Notification Bot]

Yuri de Wit has marked this topic as unresolved.