Documentation

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

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

mkLit :: Literal -> Maybe Expr Source

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

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

strengthenResult :: Var -> SpecType Source