[Agda] Strict application

Dmytro Starosud d.starosud at gmail.com
Sat Apr 26 15:42:38 CEST 2014


Hello Andrés,

That looks not really related to Agda itself, but to execution Agda code.
I suppose you are using MAlonzo backend, so you can just import
Haskell's `seq` (through pragmas) and use it in Agda code.
Please see how FFI functions and data types are imported for example.

Best regards,
Dmytro


2014-04-26 15:52 GMT+03:00 Andrés Sicard-Ramírez <asr at eafit.edu.co>:
> Hi,
>
> In Haskell, a strict application can be defined by
>
> ($!) ∷ (a → b) → a → b
> f $! x = x `seq` f x
>
> Is it possible to define a strict application in Agda?
>
> Thanks,
>
> --
> Andrés
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


More information about the Agda mailing list