Stream: Coq users

Topic: Implicit arguments of polymorphic function argument

view this post on Zulip spaceloop (Oct 29 2020 at 23:48):

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.

view this post on Zulip spaceloop (Oct 30 2020 at 00:37):

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?

view this post on Zulip Li-yao (Oct 30 2020 at 00:42):


view this post on Zulip spaceloop (Oct 30 2020 at 00:49):


Last updated: Feb 06 2023 at 13:03 UTC