-- | This is the /safe/ interface of the untrustworthy module "Example". 
module SafeExample where

import SecLib.Trustworthy 
import Downgrade
import qualified Example 

-- | Execute the function 'Example.hello'.
hello = run Example.hello

-- | It executes function 'Example.public_check' using the escape hatch 'math'.
low_check = do eh <- match 
               run $ Example.low_check eh