25.16.1.4 close

The close builtin allows you to destroy IO spaces, closing the underlying IO device. The prototype is:

fun close = (int<32> ios) void

where ios is some previously created IO space. All pending data is written to the underlying IO device.

If the IO space specified to close doesn’t exist then an E_no_ios exception is raised.

If errors occurred while closing the IO space, then E_ios exception is raised.