## Stream: new members

### Topic: What is the difference between abbreviation and def

#### Lars Ericson (Dec 10 2020 at 15:49):

What is the difference between abbreviation and def? Is abbreviation more like macro expansion with less type checking/type inference?

Is there a canonical example requiring use of abbreviation where def won't work?

I looked for abbreviation in TPIL and Logic&Proof and the Reference Manual and couldn't find it.

#### Eric Wieser (Dec 10 2020 at 15:59):

abbreviation is @[inline, reducible] def

#### Eric Wieser (Dec 10 2020 at 16:00):

I thinkalias is stronger than abbreviation

#### Mario Carneiro (Dec 10 2020 at 16:04):

alias is just a regular def/theorem

#### Mario Carneiro (Dec 10 2020 at 16:04):

I wouldn't recommend using it for defs actually

#### Mario Carneiro (Dec 10 2020 at 16:05):

I don't think there are any reasons to use abbreviation

#### Eric Wieser (Dec 10 2020 at 16:14):

alias shows up specially in doc-gen, somehow

(deleted)

#### Lars Ericson (Dec 10 2020 at 17:41):

The @[inline, reducible] has a pragmatic effect. I had a situation where abbreviation worked for something and def did not.

#### Lars Ericson (Dec 10 2020 at 17:52):

For example this works with abbreviation:

import measure_theory.lebesgue_measure
import measure_theory.borel_space
import data.set.intervals.basic
import measure_theory.measure_space

open measure_theory

noncomputable instance {α} {p : α → Prop} [m : measure_space α] : measure_space (subtype p) :=
{ volume := measure.comap (coe : _ → α) volume }

theorem subtype.volume_apply {α} {p : α → Prop} [measure_space α]
(hp : is_measurable {x | p x}) {s : set (subtype p)} (hs : is_measurable s) :
volume s = volume ((coe : _ → α) '' s) :=
measure.comap_apply _ subtype.coe_injective (λ _, is_measurable.subtype_image hp) _ hs

abbreviation I01 := (set.Icc (0 : ℝ) 1)

instance : probability_measure (volume : measure I01) :=
{ measure_univ := begin
refine (subtype.volume_apply is_measurable_Icc is_measurable.univ).trans _,
suffices : volume I01 = 1, {simpa},
rw [real.volume_Icc], simp
end }


and if I change the abbreviation to a def, I get this:

bar.lean:22:4
rewrite tactic failed, did not find instance of the pattern in the target expression
⇑volume (set.Icc ?m_1 ?m_2)
state:
⊢ ⇑volume I01 = 1


I'm guessing that's the inline or macro effect and in this case it is required to get the proof to go through.

#### Reid Barton (Dec 10 2020 at 17:53):

it's reducible

#### Reid Barton (Dec 10 2020 at 17:53):

I01 is still not a macro, it's just that more things are willing to unfold it automatically.

#### Mario Carneiro (Dec 10 2020 at 18:05):

Eric Wieser said:

alias shows up specially in doc-gen, somehow

alias is primarily intended for documentation purposes, or to make a theorem available under two names to make it easier to find (e.g. left_distrib vs mul_add)

#### Eric Wieser (Dec 10 2020 at 18:07):

Is aliasbuiltin syntax, or is it a mathlib command?

#### Mario Carneiro (Dec 10 2020 at 18:08):

https://leanprover-community.github.io/mathlib_docs/tactic/alias.html

#### Eric Wieser (Dec 10 2020 at 18:13):

What I thought was "special doc-gen treatment" was actually just this generated docstring: