Zulip Chat Archive

Stream: new members

Topic: Extract a type from an explicit instance argument

cognivore (Jun 22 2022 at 16:56):

I often find myself writing code like:

inductive I (T : Type) [Monad M] ...

It unwraps implicitly into I T M inst_monad.

Given concrete X, I can't call I X, because it needs a monad. So I need to write @I X Y my, where my captures monad instance for Y. I'm ok with it, but my intuition is that I can somehow write I (T : Type) (m : Monad M) and call I somehow in such way that Y is "inferred" from my?..

Kevin Buzzard (Jun 22 2022 at 17:01):

Just to clarify, is this Lean 4?

Kevin Buzzard (Jun 22 2022 at 17:02):

Why don't you make M explicit?

Last updated: Dec 20 2023 at 11:08 UTC