Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v2, rwe/actions-hlint-setup@v1, rwe/actions-hlint-run@v2. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, rwe/actions-hlint-setup@v1, rwe/actions-hlint-run@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

Suggestion in analyzeBind in module Data.SBV.Plugin.Analyze: Use otherwise ▫︎ Found: "condProve (b, e)\n | not $ null (sbvAnnotation b)\n = mapM_ workAnnotated (sbvAnnotation b)\n | TyCoRep.TyConApp tc _ <- varType b,\n getOccString (tyConName tc) == \"Proved\"\n = liftIO $ prove cfg [] b e\n | True = return ()\n where\n workAnnotated (SBV opts)\n | Just s <- hasSkip opts\n = liftIO\n $ putStrLn\n $ \"[SBV] \"\n ++\n showSpan (flags cfgEnv) (pickSpan [varSpan b])\n ++\n \" Skipping \" ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ \": \" ++ s\n | Uninterpret `elem` opts = return ()\n | True = liftIO $ prove cfg opts b e\n hasSkip opts = listToMaybe [s | Skip s <- opts]" ▫︎ Perhaps: "condProve (b, e)\n | not $ null (sbvAnnotation b)\n = mapM_ workAnnotated (sbvAnnotation b)\n | TyCoRep.TyConApp tc _ <- varType b,\n getOccString (tyConName tc) == \"Proved\"\n = liftIO $ prove cfg [] b e\n | otherwise = return ()\n where\n workAnnotated (SBV opts)\n | Just s <- hasSkip opts\n = liftIO\n $ putStrLn\n $ \"[SBV] \"\n ++\n showSpan (flags cfgEnv) (pickSpan [varSpan b])\n ++\n \" Skipping \" ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ \": \" ++ s\n | Uninterpret `elem` opts = return ()\n | True = liftIO $ prove cfg opts b e\n hasSkip opts = listToMaybe [s | Skip s <- opts]"

Suggestion in analyzeBind in module Data.SBV.Plugin.Analyze: Use otherwise ▫︎ Found: "workAnnotated (SBV opts)\n | Just s <- hasSkip opts\n = liftIO\n $ putStrLn\n $ \"[SBV] \"\n ++\n showSpan (flags cfgEnv) (pickSpan [varSpan b])\n ++\n \" Skipping \" ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ \": \" ++ s\n | Uninterpret `elem` opts = return ()\n | True = liftIO $ prove cfg opts b e" ▫︎ Perhaps: "workAnnotated (SBV opts)\n | Just s <- hasSkip opts\n = liftIO\n $ putStrLn\n $ \"[SBV] \"\n ++\n showSpan (flags cfgEnv) (pickSpan [varSpan b])\n ++\n \" Skipping \" ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ \": \" ++ s\n | Uninterpret `elem` opts = return ()\n | otherwise = liftIO $ prove cfg opts b e"

Suggestion in proveIt in module Data.SBV.Plugin.Analyze: Use otherwise ▫︎ Found: "runProver prop\n | qCheck = Left `fmap` S.svQuickCheck prop\n | True\n = Right\n `fmap`\n S.proveWithAny [s {S.verbose = verbose} | s <- solverConfigs] prop" ▫︎ Perhaps: "runProver prop\n | qCheck = Left `fmap` S.svQuickCheck prop\n | otherwise\n = Right\n `fmap`\n S.proveWithAny [s {S.verbose = verbose} | s <- solverConfigs] prop"

Suggestion in proveIt in module Data.SBV.Plugin.Analyze: Use otherwise ▫︎ Found: "plu\n | length finalUninterps > 1 = \"s:\"\n | True = \":\"" ▫︎ Perhaps: "plu\n | length finalUninterps > 1 = \"s:\"\n | otherwise = \":\""

Suggestion in proveIt in module Data.SBV.Plugin.Analyze: Use otherwise ▫︎ Found: "debugTrace s w\n | debug = trace (\"--> \" ++ s) w\n | True = w" ▫︎ Perhaps: "debugTrace s w\n | debug = trace (\"--> \" ++ s) w\n | otherwise = w"

Suggestion in proveIt in module Data.SBV.Plugin.Analyze: Use otherwise ▫︎ Found: "v con\n | con == integerINDataCon = - i\n | True = i" ▫︎ Perhaps: "v con\n | con == integerINDataCon = - i\n | otherwise = i"

Suggestion in mkValidName in module Data.SBV.Plugin.Analyze: Use otherwise ▫︎ Found: "genSym bad nm\n | nm `elem` bad\n = hd\n (\"genSym: \" ++ nm)\n [nm' |\n i <- [(0 :: Int) .. ],\n let nm' = nm ++ \"_\" ++ show i,\n nm' `notElem` bad]\n | True = nm" ▫︎ Perhaps: "genSym bad nm\n | nm `elem` bad\n = hd\n (\"genSym: \" ++ nm)\n [nm' |\n i <- [(0 :: Int) .. ],\n let nm' = nm ++ \"_\" ++ show i,\n nm' `notElem` bad]\n | otherwise = nm"

Suggestion in mkValidName in module Data.SBV.Plugin.Analyze: Use otherwise ▫︎ Found: "unSMT nm\n | map toLower nm `elem` S.smtLibReservedNames\n = if not (null nm) && isUpper (hd \"unSMT\" nm) then\n \"sbv\" ++ nm\n else\n \"sbv_\" ++ nm\n | True = nm" ▫︎ Perhaps: "unSMT nm\n | map toLower nm `elem` S.smtLibReservedNames\n = if not (null nm) && isUpper (hd \"unSMT\" nm) then\n \"sbv\" ++ nm\n else\n \"sbv_\" ++ nm\n | otherwise = nm"

Suggestion in mkValidName in module Data.SBV.Plugin.Analyze: Use otherwise ▫︎ Found: "escape nm\n | isAlpha (hd \"escape\" nm) && all isGood (tl \"escape\" nm) = nm\n | True = \"|\" ++ map tr nm ++ \"|\"" ▫︎ Perhaps: "escape nm\n | isAlpha (hd \"escape\" nm) && all isGood (tl \"escape\" nm) = nm\n | otherwise = \"|\" ++ map tr nm ++ \"|\""

Suggestion in pickSolvers in module Data.SBV.Plugin.Common: Use otherwise ▫︎ Found: "pickSolvers slvrs\n | AnySolver `elem` slvrs = S.getAvailableSolvers\n | True\n = case mapMaybe (`lookup` solvers) slvrs of\n [] -> return [S.defaultSMTCfg]\n xs -> return xs\n where\n solvers\n = [(Z3, S.z3), (Yices, S.yices), (Boolector, S.boolector),\n (CVC4, S.cvc4), (MathSAT, S.mathSAT), (ABC, S.abc)]" ▫︎ Perhaps: "pickSolvers slvrs\n | AnySolver `elem` slvrs = S.getAvailableSolvers\n | otherwise\n = case mapMaybe (`lookup` solvers) slvrs of\n [] -> return [S.defaultSMTCfg]\n xs -> return xs\n where\n solvers\n = [(Z3, S.z3), (Yices, S.yices), (Boolector, S.boolector),\n (CVC4, S.cvc4), (MathSAT, S.mathSAT), (ABC, S.abc)]"

The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/

The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/