spaceloop (Oct 29 2020 at 23:48): 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.
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?
Li-yao (Oct 30 2020 at 00:42):@id
spaceloop (Oct 30 2020 at 00:49):Thanks!
Last updated: Oct 05 2023 at 02:01 UTC