coreToDef :: Reftable r => LocSymbol -> Var -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon] Source #

coreToFun :: LocSymbol -> Var -> CoreExpr -> LogicM ([Var], Either Expr Expr) Source #

coreToLogic :: CoreExpr -> LogicM Expr Source #

mkLit :: Literal -> Maybe Expr Source #

mkI :: Integer -> Maybe Expr Source #

mkS :: ByteString -> Maybe Expr Source #

runToLogic :: TCEmb TyCon -> LogicMap -> DataConMap -> (String -> Error) -> LogicM t -> Either Error t Source #

runToLogicWithBoolBinds :: [Var] -> TCEmb TyCon -> LogicMap -> DataConMap -> (String -> Error) -> LogicM t -> Either Error t Source #

logicType :: Reftable r => Type -> RRType r Source #

strengthenResult :: Var -> SpecType Source #

strengthenResult' :: Var -> SpecType Source #

normalize :: Simplify a => a -> a Source #