Type alias

Stream: new members

[Jason Orendorff]

I had

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]

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

[Kevin Buzzard]

You could make the def @[reducible]

[Kevin Buzzard]

but that might not fix the type class problem

[Patrick Massot]

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

[Patrick Massot]

Could you tell us about your end goal here?

[Reid Barton]

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

[Jason Orendorff]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Guilherme Espada]

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]

What does #check finmap say?

[Johan Commelin]

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

[Johan Commelin]

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

[Guilherme Espada]

Abbreviation works! Thank you