@@ -156,8 +156,8 @@ dumpState ist inElab menv ps | [] <- holes ps =
156156 iputGoal rendered
157157dumpState ist inElab menv ps | (h : hs) <- holes ps = do
158158 let OK ty = goalAtFocus ps
159− let OK env = envAtFocus ps
160− let state = prettyOtherGoals hs <> line <>
159+ OK env = envAtFocus ps
160+ state = prettyOtherGoals hs <> line <>
161161 prettyAssumptions inElab ty env <> line <>
162162 prettyMetaValues (reverse menv) <>
163163 prettyGoal (zip (assumptionNames env) (repeat False)) ty
@@ -215,21 +215,19 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do
215215 bindingOf h False <+> colon <+> align (prettyG bnd ty)
216216
217217 prettyAssumptions inElab g env =
218− if length env == 0 then
219− empty
218+ if null env then empty
220219 else
221220 text "---------- Assumptions: ----------" <>
222221 nest nestingSize (prettyPs inElab g [] $ reverse env)
223222
224223 prettyOtherGoals hs =
225− if length hs == 0 then
226− empty
224+ if null hs then empty
227225 else
228226 text "---------- Other goals: ----------" <$$>
229− nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
227+ nest nestingSize (align . cat . punctuate (text ",") . map (`bindingOf` False) $ hs)
230228
231229 freeEnvNames :: Env -> [Name]
232− freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))
230+ freeEnvNames = concatMap (\(n, b) -> freeNames (Bind n b Erased))
233231
234232lifte :: ElabState EState -> ElabD a -> Idris a
235233lifte st e = do (v, _) <- elabStep st e
@@ -247,7 +245,7 @@ receiveInput h e =
247245 (sexp, id) <- case IdeMode.parseMessage l of
248246 Left err -> ierror err
249247 Right (sexp, id) -> return (sexp, id)
250− putIState $ i { idris_outputmode = (IdeMode id h) }
248+ putIState $ i { idris_outputmode = IdeMode id h }
251249 case IdeMode.sexpToCommand sexp of
252250 Just (IdeMode.REPLCompletions prefix) ->
253251 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
@@ -309,7 +307,7 @@ elabloop fn d prompt prf e prev h env
309307 Success (Left cmd') ->
310308 case cmd' of
311309 EQED -> do hs <- lifte e get_holes
312− when (not (null hs)) $ ifail "Incomplete proof"
310+ unless (null hs) $ ifail "Incomplete proof"
313311 iputStrLn "Proof completed!"
314312 return (False, prev, e, True, prf, env, Right $ iPrintResult "")
315313 EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev
@@ -333,8 +331,8 @@ elabloop fn d prompt prf e prev h env
333331 return (d', prev, st', done, prf', env, go)
334332 Success (Right cmd') ->
335333 case cmd' of
336− DoLetP _ _ _ -> ifail "Pattern-matching let not supported here"
337− DoBindP _ _ _ _ -> ifail "Pattern-matching <- not supported here"
334+ DoLetP {} -> ifail "Pattern-matching let not supported here"
335+ DoBindP {} -> ifail "Pattern-matching <- not supported here"
338336 DoLet fc i ifc Placeholder expr ->
339337 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
340338 ctxt <- getContext
@@ -380,7 +378,7 @@ elabloop fn d prompt prf e prev h env
380378 else do ok
381379 elabloop fn d prompt prf' st prev' h' env'
382380
383− where
381+ where
384382 -- A bit of a hack: wrap the value up in a let binding, which will
385383 -- normalise away. It would be better to figure out how to call
386384 -- the elaborator with a custom environment here to avoid the
@@ -412,7 +410,7 @@ ploop fn d prompt prf e h
412410 return (i, h)
413411 (cmd, step) <- case x of
414412 Nothing -> do iPrintError ""; ifail "Abandoned"
415− Just input -> do return (parseTactic i input, input)
413+ Just input -> return (parseTactic i input, input)
416414 case cmd of
417415 Success Abandon -> do iPrintError ""; ifail "Abandoned"
418416 _ -> return ()
@@ -426,7 +424,7 @@ ploop fn d prompt prf e h
426424 iputStrLn $ "TT: " ++ show tm ++ "\n"
427425 return (False, e, False, prf, Right $ iPrintResult "")
428426 Success Qed -> do hs <- lifte e get_holes
429− when (not (null hs)) $ ifail "Incomplete proof"
427+ unless (null hs) $ ifail "Incomplete proof"
430428 iputStrLn "Proof completed!"
431429 return (False, e, True, prf, Right $ iPrintResult "")
432430 Success (TCheck (PRef _ _ n)) -> checkNameType e prf n