Fun #Agda
Conversation
not fully used to quantifying with (x : A) ->
1
I’m pretty sure you can use `{xx : Type} -> ...` without the `forall` here if you wanted to pass things implicitly. Not sure how parametericity is handled in Agda though - `forall` might be important for marking the parameter as irrelevant.
1
yeah but Haskell can do that! I wanted to use (xx : Type) -> .. (aka forall (xx :: Type) -> ...) until the future happens :p
1
1
Replying to
Right, understood! Yeah, dependent functions are soo cool! 🤩🤩🤩