How do I access unnamed instances?

Stream: general

[nrs]

I'd like to grab a CoreM inhabitant and I saw that it has an Inhabited instance, but it's not named. How can I access unnamed instances?

[Kyle Miller]

docs#inferInstance is a basic tool for this

[nrs]

Kyle Miller said:

docs#inferInstance is a basic tool for this

Thanks a lot for the reference!

[Kyle Miller]

But also, it's worth checking what you're trying to do with the instance

[nrs]

hm yeah default inhabitants aren't usually very interesting (in the Inhabited instance case)

[Kyle Miller]

There's also docs#Inhabited.default for Inhabited in particular. It's exported, so you can refer to it with just default.

[Kyle Miller]

example : Nat := default

[nrs]

Kyle Miller said:

There's also docs#Inhabited.default for Inhabited in particular. It's exported, so you can refer to it with just default.

Ah neat! thank you very much!!