@@ -27,6 +27,7 @@ import System.IO
2727import Data.Char
2828import Data.Maybe (fromMaybe)
2929
30+import Debug.Trace
3031
3132caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
3233caseSplitAt h fn updatefile l n
@@ -248,12 +249,15 @@ makeLemma h fn updatefile l n
248249 [] -> ierror (NoSuchVariable n)
249250 ns -> ierror (CantResolveAlts (map fst ns))
250251 i <- getIState
252+ margs <- case lookup n (idris_metavars i) of
253+ Just (_, arity, _) -> return arity
254+ _ -> return (-1)
251255
252256 if (not isProv) then do
253257 let skip = guessImps (tt_ctxt i) mty
254258
255259 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
256− let lem_app = show n ++ appArgs skip mty
260+ let lem_app = show n ++ appArgs skip margs mty
257261
258262 if updatefile then
259263 do let fb = fn ++ "~"
@@ -271,7 +275,7 @@ makeLemma h fn updatefile l n
271275 in runIO . hPutStrLn h $ convSExp "return" good n
272276
273277 else do -- provisional definition
274− let lem_app = show n ++ appArgs [] mty ++
278+ let lem_app = show n ++ appArgs [] (-1) mty ++
275279 " = ?" ++ show n ++ "_rhs"
276280 if updatefile then
277281 do let fb = fn ++ "~"
@@ -288,15 +292,17 @@ makeLemma h fn updatefile l n
288292
289293 where getIndent s = length (takeWhile isSpace s)
290294
291− appArgs skip (Bind n@(UN c) (Pi _) sc)
292− | thead c /= '_' && n `notElem` skip
293− = " " ++ show n ++ appArgs skip sc
294− appArgs skip (Bind _ (Pi _) sc) = appArgs skip sc
295− appArgs skip _ = ""
295+ appArgs skip 0 _ = ""
296+ appArgs skip i (Bind n@(UN c) (Pi _) sc)
297+ | (thead c /= '_' && n `notElem` skip)
298+ = " " ++ show n ++ appArgs skip (i - 1) sc
299+ appArgs skip i (Bind _ (Pi _) sc) = appArgs skip (i - 1) sc
300+ appArgs skip i _ = ""
296301
297302 stripMNBind skip (PPi b n@(UN c) ty sc)
298− | thead c /= '_' &&
299− n `notElem` skip = PPi b n ty (stripMNBind skip sc)
303+ | (thead c /= '_' && n `notElem` skip) ||
304+ take 4 (str c) == "__pi" -- keep in type, but not in app
305+ = PPi b n ty (stripMNBind skip sc)
300306 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
301307 stripMNBind skip t = t
302308