@@ -348,6 +348,27 @@ Usage from C code
348348 return result;
349349 }
350350
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
355+copy it over.
356+
357+.. code-block:: idris
358+
359+ getString : () -> IO (Raw String)
360+ getString () = foreign FFI_C "get_string" (IO (Raw String))
361+
362+.. code-block:: cpp
363+
364+ const VAL get_string ()
365+ {
366+ char * c_string = get_string_allocated_with_malloc()
367+ const VAL idris_string = MKSTR(c_string);
368+ free(c_string);
369+ return idris_string
370+ }
371+
351372FFI implementation
352373------------------
353374