Skip to content

Commit

Permalink
make hlint happy
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed Jan 3, 2024
1 parent 4f2e9e5 commit 8273a13
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 1 deletion.
2 changes: 1 addition & 1 deletion Data/SBV/Control/Utils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -427,7 +427,7 @@ class (HasKind r, SatModel r) => SMTFunction fun a r | fun -> a r where
(sv, SBVApp (Uninterpreted nm) _) | r == sv -> return nm
_ -> cantFind uiMap

sexprToFun f (s, e) = do nm <- (fst . fst) <$> smtFunName f
sexprToFun f (s, e) = do nm <- fst . fst <$> smtFunName f
mbRes <- case parseSExprFunction e of
Just (Left nm') -> case (nm == nm', smtFunDefault f) of
(True, Just v) -> return $ Just ([], v)
Expand Down
2 changes: 2 additions & 0 deletions Documentation/SBV/Examples/ProofTools/AddHorn.hs
Original file line number Diff line number Diff line change
Expand Up @@ -98,3 +98,5 @@ verify = prove vcs
vcs = quantifiedBool (vc1 invariant)
.&& quantifiedBool (vc3 invariant)
.&& quantifiedBool (vc3 invariant)

{- HLint ignore quantify "Redundant lambda" -}

0 comments on commit 8273a13

Please sign in to comment.