| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Language.Lean.Internal.String
Description
This module exports functions for marshalling strings across the Lean FFI.
- mkLeanString :: IO CString -> IO String
- mkLeanText :: IO CString -> IO Text
- getLeanString :: CString -> IO String
- decodeLeanString :: CString -> IO String
- withLeanStringPtr :: String -> (CString -> IO a) -> IO a
- withLeanTextPtr :: Text -> (CString -> IO a) -> IO a
Documentation
mkLeanString :: IO CString -> IO String Source
This calls a function that allocates a Lean string, parses it as
a Text value, and frees the string.
mkLeanText :: IO CString -> IO Text Source
This calls a function that allocates a Lean string, parses it as
a Text value, and frees the string.
getLeanString :: CString -> IO String Source
This calls a function that allocates a Lean string, parses it as
a Text value, and frees the string.
decodeLeanString :: CString -> IO String Source
This decodes a CString as Lean text