@@ -348,6 +348,27 @@ Usage from C code
348 return result;
348 return result;
351+The ``Raw`` type constructor allows you to access or return a runtime
352+representation of the value. For instance, if you want to copy a string
353+generated from C code into an Idris value, you may want to return a
354+``Raw String``instead of a ``String`` and use ``MKSTR`` or ``MKSTRlen`` to
357+.. code-block:: idris
359+ getString : () -> IO (Raw String)
360+ getString () = foreign FFI_C "get_string" (IO (Raw String))
364+ const VAL get_string ()
366+ char * c_string = get_string_allocated_with_malloc()
367+ const VAL idris_string = MKSTR(c_string);
351FFI implementation
372FFI implementation
352------------------
373------------------