@@ -347,6 +347,27 @@ Usage from C code
347 return result;
347 return result;
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
356+.. code-block:: idris
358+ getString : () -> IO (Raw String)
359+ getString () = foreign FFI_C "get_string" (IO (Raw String))
363+ const VAL get_string ()
365+ char * c_string = get_string_allocated_with_malloc()
366+ const VAL idris_string = MKSTR(c_string);
350FFI implementation
371FFI implementation
351------------------
372------------------