@@ -360,27 +360,27 @@ irTerm vs env tm@(App f a) = case unApply tm of
361 applyName :: Name -> IState -> [Term] -> Idris LExp
361 applyName :: Name -> IState -> [Term] -> Idris LExp
362 applyName n ist args =
362 applyName n ist args =
363− LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
363+ LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
365− erase (i, x)
365+ erase (i, x)
366− | i >= arity || i `elem` used = x
366+ | i >= arity || i `elem` used = x
367− | otherwise = Erased
367+ | otherwise = Erased
369− arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
369+ arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
370− Just (CaseOp ci ty tys def tot cdefs) -> length tys
370+ Just (CaseOp ci ty tys def tot cdefs) -> length tys
371− Just (TyDecl (DCon tag ar) _) -> ar
371+ Just (TyDecl (DCon tag ar) _) -> ar
372− Just (TyDecl Ref ty) -> length $ getArgTys ty
372+ Just (TyDecl Ref ty) -> length $ getArgTys ty
373− Just (Operator ty ar op) -> ar
373+ Just (Operator ty ar op) -> ar
374− Just def -> error $ "unknown arity: " ++ show (n, def)
374+ Just def -> error $ "unknown arity: " ++ show (n, def)
375− Nothing -> 0 -- no definition, probably local name => can't erase anything
375+ Nothing -> 0 -- no definition, probably local name => can't erase anything
377− -- name for purposes of usage info lookup
377+ -- name for purposes of usage info lookup
379− | Just n' <- viMethod =<< M.lookup n vs = n'
379+ | Just n' <- viMethod =<< M.lookup n vs = n'
380− | otherwise = n
380+ | otherwise = n
382− used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
382+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
383− fst4 (x,_,_,_) = x
383+ fst4 (x,_,_,_) = x
385irTerm vs env (P _ n _) = return $ LV (Glob n)
385irTerm vs env (P _ n _) = return $ LV (Glob n)
386irTerm vs env (V i)
386irTerm vs env (V i)