Zulip Chat Archive

Stream: lean4

Topic: def vs abbrev


Yuri de Wit (Jun 20 2022 at 21:44):

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 (Jun 20 2022 at 21:49):

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 (Jun 21 2022 at 15:32):

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 (Jun 21 2022 at 15:53):

Yuri de Wit has marked this topic as unresolved.


Last updated: Dec 20 2023 at 11:08 UTC