You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently agda2hs assumes that all non-erased module parameters are types and should be compiled to explicit foralls. For example:
module_ (x : Int) wherefoo : Int
foo = x
{-# COMPILE AGDA2HS foo #-}
is compiled to
foo::forallx.Int
foo = x
We should either compile the module parameter to a regular function argument, or else throw an error that non-type module parameters are not supported.
The text was updated successfully, but these errors were encountered:
Currently
agda2hs
assumes that all non-erased module parameters are types and should be compiled to explicitforalls
. For example:is compiled to
We should either compile the module parameter to a regular function argument, or else throw an error that non-type module parameters are not supported.
The text was updated successfully, but these errors were encountered: