[Agda] Strict application

[Dmytro Starosud]

(here you can see how it looks
http://www.cse.chalmers.se/~nad/listings/lib-0.7/IO.Primitive.html)

2014-04-26 16:42 GMT+03:00 Dmytro Starosud <d.starosud at gmail.com>:
> 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
>>