@@ -347,6 +347,27 @@ Usage from C code
347347 return result;
348348 }
349349
350+The ``Raw`` type constructor allows you to access or return a runtime
351+representation of the value. For instance, if you want to copy a string
352+generated from C code into an Idris value, you may want to return a
353+``Raw String``instead of a ``String`` and use ``MKSTR`` or ``MKSTRlen`` to
354+copy it over.
355+
356+.. code-block:: idris
357+
358+ getString : () -> IO (Raw String)
359+ getString () = foreign FFI_C "get_string" (IO (Raw String))
360+
361+.. code-block:: cpp
362+
363+ const VAL get_string ()
364+ {
365+ char * c_string = get_string_allocated_with_malloc()
366+ const VAL idris_string = MKSTR(c_string);
367+ free(c_string);
368+ return idris_string
369+ }
370+
350371FFI implementation
351372------------------
352373