Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: ee004b1c by Jonathan Graveline at 2018-06-14T02:28:53Z Added Ref_make, Ref_read, Ref_write - - - - -

1 changed file:

- btl/builtins.typer

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -229,4 +229,13 @@ File_read = Built-in "File.read" : FileHandle -> Int -> IO String; Sys_cpu_time = Built-in "Sys.cpu_time" : Unit -> IO Float; Sys_exit = Built-in "Sys.exit" : Int -> IO Unit;

+%% Ref (modifiable value) + +% Ref : Type -> Type; +% Ref = typecons (Ref (a : Type)) (Ref a); + +Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a); +Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a; +Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit; + %%% builtins.typer ends here.

View it on GitLab: https://gitlab.com/monnier/typer/commit/ee004b1c893a143e8801e9d60cfd36bfbaff...