Documentation

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

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

coreToLogic :: CoreExpr -> LogicM Expr Source

coreToPred :: CoreExpr -> LogicM Expr Source

mkLit :: Literal -> Maybe Expr Source

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

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

strengthenResult :: Var -> SpecType Source