Language.Lean.Internal.Exception.Unsafe

Operations for getting Lean values from functions that must not have side effects.

Documentation

tryGetEnum :: Enum a => LeanPartialFn CInt -> a

Try to run a Lean partial function that returns an enum type

Other than allocating a new value or throwing an exception, the function should be pure.

tryGetLeanValue :: IsLeanValue a p => LeanPartialFn p -> a

Try to run a Lean partial function that returns a Lean value that will need to be freed.

Other than allocating a new value or exception, the function should be be pure.

tryGetLeanMaybeValue :: IsLeanValue a p => LeanPartialFn p -> Maybe a

Try to run a Lean function that may return a Lean value that will need to be freed.

Other than allocating a new value or throwing an exception, the function should be pure.