## Stream: general

### Topic: abbreviation

#### Reid Barton (Dec 03 2018 at 02:46):

I don't suppose abbreviation is documented anywhere?

#### Reid Barton (Dec 03 2018 at 02:46):

It seems to do something very specific that I want (MWE incoming)

#### Reid Barton (Dec 03 2018 at 02:48):

def test1 {α : Type} [has_add α] (x : α) := x + x
def test2 {α : Type} [my_add α] (x : α) := x + x -- failed to synthesize type class instance for has_add α
def test3 {α : Type} [my_add' α] (x : α) := x + x -- ok!


#### Reid Barton (Dec 03 2018 at 02:48):

Is there a catch?

#### Reid Barton (Dec 03 2018 at 02:50):

You can also do more interesting things like abbreviation my_add' (α : Type) := has_add (list α)

#### Sebastien Gouezel (Dec 28 2019 at 18:57):

I have tried to convert module to an abbreviation for semimodule, but something is not working out of the box. Here is a minimal example showing the problem.

import algebra.pi_instances

universes u v w

class SemiModule (β : Type v) [add_comm_monoid β]

abbreviation Module (β : Type v) [add_comm_group β] :=
SemiModule β

instance piSemiModule (I : Type w) (f : I → Type u)
[∀ i, add_comm_monoid $f i] [∀ i, SemiModule (f i)] : SemiModule (Π i : I, f i) := by constructor instance piModule (I : Type w) (f : I → Type u) [∀ i, add_comm_group$ f i] [∀ i, Module (f i)] :
Module (Π i : I, f i) := by apply_instance


The last by apply_instance does not find the instance piSemiModule which is right here. I don't understand why.

#### Kevin Buzzard (Dec 29 2019 at 15:03):

import algebra.pi_instances

universes u v w

class SemiModule (β : Type v) [add_comm_monoid β]

abbreviation Module (β : Type v) [add_comm_group β] :=
SemiModule β

instance piSemiModule (I : Type w) (f : I → Type u)
[∀ i, add_comm_monoid $f i] [∀ i, SemiModule (f i)] : SemiModule (Π i : I, f i) := by constructor instance piSemiModule' (I : Type w) (f : I → Type u) [∀ i, add_comm_monoid$ f i] [∀ i, SemiModule (f i)] :
SemiModule (Π i : I, f i) := by apply_instance -- works

instance piModule (I : Type w) (f : I → Type u)


#### Chris Hughes (Dec 29 2019 at 17:16):

I might be completely wrong.

#### Chris Hughes (Dec 29 2019 at 17:18):

It must be trying to unify

@SemiModule (Π (i : ?M_1), ?M_2 i) (@pi.add_comm_monoid ?M_1 (λ (i : ?M_1), ?M_2 i) (λ (i : ?M_1), ?M_3 i))


with

@SemiModule (Π (i : I), f i)
(@pi.add_comm_group I (λ (i : I), f i) (λ (i : I), _inst_1 i)))


#### Chris Hughes (Dec 29 2019 at 17:18):

Which is difficult with the metavariables there.

#### Chris Hughes (Dec 29 2019 at 17:21):

?M_1 and ?M_2 look easy to infer, but ?M_3 must be the difficult one.

#### Chris Hughes (Dec 29 2019 at 17:22):

And you have to unfold ?M_3 to see that they are defeq.

#### Chris Hughes (Dec 29 2019 at 17:42):

I guess this maybe answers the question you asked me the other day about extending type classes, versus having the other class as an argument. This seems to be a downside of the argument approach.

#### Paul van Wamelen (Jan 23 2021 at 19:59):

Is there documentation for abbreviation?

#### Paul van Wamelen (Jan 23 2021 at 20:14):

Oh: "abbreviation is indeed a synonym for @[inline, reducible] def" (from Mario a while ago)

Last updated: May 16 2021 at 21:11 UTC