Zulip Chat Archive

Stream: new members

Topic: Unfold typeclass instance

Bhavik Mehta (Jun 08 2020 at 22:46):

Is there a way in which I can use the particular definition of a typeclass instance - in my case I want the actual definition of pullback.fst in the category of types

Reid Barton (Jun 08 2020 at 22:47):

Do you mean unfold the definition?

Bhavik Mehta (Jun 08 2020 at 22:47):

Yeah I guess so

Reid Barton (Jun 08 2020 at 22:47):

They have autogenerated names

Bhavik Mehta (Jun 08 2020 at 22:47):

dunfold and dsimp didn't go far enough

Bhavik Mehta (Jun 08 2020 at 22:48):

ah never mind I got dunfold to do it

Last updated: Dec 20 2023 at 11:08 UTC