idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Force/Delay need to be inlined in Builtins

Browse Source 
Otherwise (especially in the case of delay) the argument might be
evaluated prematurely.
This commit is contained in:
Edwin Brady 2020-12-06 20:00:48 +00:00
parent 22a534f400
commit 63a46722ef
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libs/prelude/Builtin.idr
View File

@ -186,11 +186,11 @@ export partial
idris_crash : String -> a
idris_crash = prim__crash _
public export
public export %inline
delay : a -> Lazy a
delay x = Delay x
public export
public export %inline
force : Lazy a -> a
force x = Force x