Idris2Doc : Compiler.String

Compiler.String

For internal spidr use only.

Definitions

dataCppString : Type
Totality: total
Visibility: public export
Constructor: 
MkCppString : AnyPtr->CppString
prim__mkString : PrimIOAnyPtr
cppString : HasIOio=>ioCppString
  It is up to the caller to `delete` the string.

Totality: total
Visibility: export
prim__stringDelete : AnyPtr->PrimIO ()
delete : HasIOio=>CppString->io ()
Totality: total
Visibility: export
c_str : CppString->String
Totality: total
Visibility: export
prim__stringData : AnyPtr->PtrChar
prim__stringSize : AnyPtr->Bits64