@@ -76,7 +76,7 @@ addClauseFrom fn updatefile l n = do
7676 getIndent i n xs | take 9 xs == "instance " = i
7777 getIndent i n xs | take (length n) xs == n = i
7878 getIndent i n (x : xs) = getIndent (i + 1) n xs
79−
79+
8080 getAppName (PApp _ r _) = getAppName r
8181 getAppName (PRef _ _ r) = r
8282 getAppName (PTyped n _) = getAppName n
@@ -120,7 +120,7 @@ addMissing fn updatefile l n
120120 if updatefile
121121 then do let fb = fn ++ "~"
122122 runIO $ writeSource fb (unlines (before ++ nonblank)
123− ++ extras ++
123+ ++ extras ++
124124 (if null extras then ""
125125 else "\n" ++ unlines rest))
126126 runIO $ copyFile fb fn
@@ -193,7 +193,7 @@ makeCase fn updatefile l n
193193 case findSubstr ('?':n) line of
194194 Just (before, pos, after) ->
195195 [before ++ (if b then "(" else "") ++ "case _ of",
196− take (pos + (if b then 6 else 5)) (repeat ' ') ++
196+ take (pos + (if b then 6 else 5)) (repeat ' ') ++
197197 "case_val => ?" ++ n ++ (if b then ")" else "")
198198 ++ after]
199199 Nothing -> fail "No such metavariable"
@@ -208,7 +208,7 @@ makeCase fn updatefile l n
208208
209209 findSubstr n xs = findSubstr' [] 0 n xs
210210
211− findSubstr' acc i n xs | take (length n) xs == n
211+ findSubstr' acc i n xs | take (length n) xs == n
212212 = Just (reverse acc, i, drop (length n) xs)
213213 findSubstr' acc i n [] = Nothing
214214 findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs
@@ -217,7 +217,7 @@ makeCase fn updatefile l n
217217
218218
219219
220−doProofSearch :: FilePath -> Bool -> Bool ->
220+doProofSearch :: FilePath -> Bool -> Bool ->
221221 Int -> Name -> [Name] -> Maybe Int -> Idris ()
222222doProofSearch fn updatefile rec l n hints Nothing
223223 = doProofSearch fn updatefile rec l n hints (Just 20)
@@ -230,7 +230,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)
230230 [] -> return n
231231 ns -> ierror (CantResolveAlts ns)
232232 i <- getIState
233− let (top, envlen, psnames, _)
233+ let (top, envlen, psnames, _)
234234 = case lookup mn (idris_metavars i) of
235235 Just (t, e, ns, False) -> (t, e, ns, False)
236236 _ -> (Nothing, 0, [], True)
@@ -281,7 +281,7 @@ updateMeta ('?':cs) n new
281281 (mv, []) -> if (mv == n) then new else '?' : mv
282282updateMeta ('=':'>':cs) n new = '=':'>':updateMeta cs n new
283283updateMeta ('=':cs) n new = '=':updateMeta cs n new
284−updateMeta (c:cs) n new
284+updateMeta (c:cs) n new
285285 = c : updateMeta cs n new
286286updateMeta [] n new = ""
287287
@@ -296,7 +296,7 @@ guessBrackets brack ('?':cs) n new
296296guessBrackets brack ('=':'>':cs) n new = guessBrackets False cs n new
297297guessBrackets brack ('-':'>':cs) n new = guessBrackets False cs n new
298298guessBrackets brack ('=':cs) n new = guessBrackets False cs n new
299−guessBrackets brack (c:cs) n new
299+guessBrackets brack (c:cs) n new
300300 = guessBrackets (brack || not (isSpace c)) cs n new
301301guessBrackets brack [] n new = ""
302302
@@ -308,7 +308,7 @@ checkProv line n = isProv' False line n
308308 isProv' _ ('}':cs) n = isProv' True cs n
309309 isProv' p (_:cs) n = isProv' p cs n
310310 isProv' _ [] n = False
311−
311+
312312addBracket False new = new
313313addBracket True new@('(':xs) | last xs == ')' = new
314314addBracket True new | any isSpace new = '(' : new ++ ")"
@@ -322,7 +322,7 @@ makeLemma fn updatefile l n
322322
323323 -- if the name is in braces, rather than preceded by a ?, treat it
324324 -- as a lemma in a provisional definition
325−
325+
326326 let isProv = checkProv tyline (show n)
327327
328328 ctxt <- getContext
@@ -339,7 +339,7 @@ makeLemma fn updatefile l n
339339 let skip = guessImps i (tt_ctxt i) mty
340340 let classes = guessClasses i (tt_ctxt i) mty
341341
342− let lem = show n ++ " : " ++
342+ let lem = show n ++ " : " ++
343343 constraints i classes mty ++
344344 showTmOpts (defaultPPOption { ppopt_pinames = True })
345345 (stripMNBind skip margs (delab i mty))
@@ -379,14 +379,14 @@ makeLemma fn updatefile l n
379379 where getIndent s = length (takeWhile isSpace s)
380380
381381 appArgs skip 0 _ = ""
382− appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)
382+ appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)
383383 | (thead c /= '_' && n `notElem` skip)
384384 = " " ++ show n ++ appArgs skip (i - 1) sc
385385 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc
386386 appArgs skip i _ = ""
387387
388388 stripMNBind _ args t | args <= 0 = t
389− stripMNBind skip args (PPi b n@(UN c) _ ty sc)
389+ stripMNBind skip args (PPi b n@(UN c) _ ty sc)
390390 | n `notElem` skip ||
391391 take 4 (str c) == "__pi" -- keep in type, but not in app
392392 = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)
@@ -399,7 +399,7 @@ makeLemma fn updatefile l n
399399 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "
400400
401401 showConstraints i ns (Bind n (Pi _ ty _) sc)
402− | n `elem` ns = show (delab i ty) :
402+ | n `elem` ns = show (delab i ty) :
403403 showConstraints i ns (substV (P Bound n Erased) sc)
404404 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)
405405 showConstraints _ _ _ = []
@@ -410,10 +410,10 @@ makeLemma fn updatefile l n
410410 -- Also, make type class instances implicit
411411 guessImps :: IState -> Context -> Term -> [Name]
412412 -- machine names aren't lifted
413− guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)
413+ guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)
414414 = n : guessImps ist ctxt sc
415415 guessImps ist ctxt (Bind n (Pi _ ty _) sc)
416− | guarded ctxt n (substV (P Bound n Erased) sc)
416+ | guarded ctxt n (substV (P Bound n Erased) sc)
417417 = n : guessImps ist ctxt sc
418418 | isClass ist ty
419419 = n : guessImps ist ctxt sc
@@ -421,11 +421,11 @@ makeLemma fn updatefile l n
421421 | ignoreName n = n : guessImps ist ctxt sc
422422 | otherwise = guessImps ist ctxt sc
423423 guessImps ist ctxt _ = []
424−
424+
425425 paramty (TType _) = True
426426 paramty (Bind _ (Pi _ (TType _) _) sc) = paramty sc
427427 paramty _ = False
428−
428+
429429 -- TMP HACK unusable name so don't lift
430430 ignoreName n = case show n of
431431 "_aX" -> True
@@ -444,7 +444,7 @@ makeLemma fn updatefile l n
444444 Just _ -> True
445445 _ -> False
446446 | otherwise = False
447−
447+
448448 isParamClass ist t
449449 | (P _ n _, args) <- unApply t
450450 = case lookupCtxtExact n (idris_classes ist) of
@@ -460,14 +460,14 @@ makeLemma fn updatefile l n
460460 isConName f ctxt = any (guarded ctxt n) args
461461-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
462462-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
463− guarded ctxt n (Bind _ (Pi _ t _) sc)
463+ guarded ctxt n (Bind _ (Pi _ t _) sc)
464464 = guarded ctxt n t || guarded ctxt n sc
465465 guarded ctxt n _ = False
466466
467467 blank = all isSpace
468468
469469 addLem before tyline lem lem_app later
470− = let (bef_end, blankline : bef_start)
470+ = let (bef_end, blankline : bef_start)
471471 = case span (not . blank) (reverse before) of
472472 (bef, []) -> (bef, "" : [])
473473 x -> x
@@ -481,6 +481,6 @@ makeLemma fn updatefile l n
481481 = case span (not . blank) later of
482482 (bef, []) -> (bef, "" : [])
483483 x -> x in
484− unlines $ before ++ tyline :
484+ unlines $ before ++ tyline :
485485 (later_bef ++ [blankline, lem_app, blankline] ++
486486 later_end)