## Stream: new members

### Topic: Type alias

#### Jason Orendorff (Jun 16 2020 at 15:00):

def env : Type := list formula

but I had trouble later using an env as a list; I would get, for example, "failed to synthesize type class instance for has_mem formula env". Switching to this made some things work:

notation env := list formula

I also found that I could def as_list (e : env) : list formula := e in namespace env and use that as a hint to Lean whenever it fails to "see through" the definition of env.

Is there a better way to do this?

#### Patrick Massot (Jun 16 2020 at 15:01):

Yes, type class resolution won't see through such aliases (that's a feature, not a bug).

#### Kevin Buzzard (Jun 16 2020 at 15:01):

You could make the def @[reducible]

#### Kevin Buzzard (Jun 16 2020 at 15:02):

but that might not fix the type class problem

#### Patrick Massot (Jun 16 2020 at 15:02):

We can teach you how to still get your instances, but that's probably a #xy issue.

#### Reid Barton (Jun 16 2020 at 15:44):

Most likely you should just copy the specific instances you're interested in (has_mem I guess).

#### Jason Orendorff (Jun 16 2020 at 17:34):

Thanks. My end goal is super dumb, I was just trying stuff

#### Scott Morrison (Jun 17 2020 at 00:34):

You can also copy the instances you care about using derive.

#### Scott Morrison (Jun 17 2020 at 00:35):

e.g. @[derive has_mem] before the def.

#### Guilherme Espada (Mar 10 2021 at 15:38):

Given a type such as finmap (λ x:string, string) how can I create a type alias, so I can refer to the type without writing it out every time.

I tried simply def'ing it def ctxtype := finmap (λ x:string, ttype), however this then prevents me from using the \in operator. Ideally I'd like to be able to use this operator with the type alias.

#### Johan Commelin (Mar 10 2021 at 15:39):

What does #check finmap say?

#### Johan Commelin (Mar 10 2021 at 15:40):

Aah, I guess you would have to define an instance to re-enable the notation again.

#### Johan Commelin (Mar 10 2021 at 15:40):

Does abbreviation ctxtype := .... help here?

#### Guilherme Espada (Mar 10 2021 at 15:46):

Abbreviation works! Thank you

Last updated: May 17 2021 at 22:15 UTC