Hi, beginner question, I hope this is the right place to ask: for a top-level definition, I can define which arguments are implicit. But how do I do this for a polymorphic function argument? E.g. `fun (id : forall a, a -> a) => id _ 3`

. I often find myself calling functions like id with _ because a is known from the context.

I've learned that I can just use `forall {a}`

. Another related question I have is, functions that are defined with implicit arguments, such as `id`

in Equations have types with existential variables, for example: `id : ?A -> ?A where ?A : [ |- Type]`

. However I'd like to use such a function as a normal polymorphic type, i.e. `forall A, A -> A`

, is that possible?

`@id`

Thanks!

Last updated: Oct 05 2023 at 02:01 UTC