Zulip Chat Archive

Stream: new members

Topic: Type alias


view this post on Zulip Jason Orendorff (Jun 16 2020 at 15:00):

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?

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:01):

You could make the def @[reducible]

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:02):

but that might not fix the type class problem

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 16 2020 at 15:02):

Could you tell us about your end goal here?

view this post on Zulip 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).

view this post on Zulip Jason Orendorff (Jun 16 2020 at 17:34):

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

view this post on Zulip Scott Morrison (Jun 17 2020 at 00:34):

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

view this post on Zulip Scott Morrison (Jun 17 2020 at 00:35):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:39):

What does #check finmap say?

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:40):

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

view this post on Zulip Johan Commelin (Mar 10 2021 at 15:40):

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

view this post on Zulip Guilherme Espada (Mar 10 2021 at 15:46):

Abbreviation works! Thank you


Last updated: May 17 2021 at 22:15 UTC