@@ -337,12 +337,13 @@ makeLemma fn updatefile l n
338 if (not isProv) then do
338 if (not isProv) then do
339 let skip = guessImps i (tt_ctxt i) mty
339 let skip = guessImps i (tt_ctxt i) mty
340+ let impty = stripMNBind skip margs (delab i mty)
340− let classes = guessClasses i (tt_ctxt i) mty
341+ let classes = guessClasses i (tt_ctxt i) [] (allNamesIn impty) mty
342 let lem = show n ++ " : " ++
343 let lem = show n ++ " : " ++
343 constraints i classes mty ++
344 constraints i classes mty ++
344 showTmOpts (defaultPPOption { ppopt_pinames = True })
345 showTmOpts (defaultPPOption { ppopt_pinames = True })
345− (stripMNBind skip margs (delab i mty))
346+ impty
346 let lem_app = guessBrackets False tyline (show n) (show n ++ appArgs skip margs mty)
347 let lem_app = guessBrackets False tyline (show n) (show n ++ appArgs skip margs mty)
348 if updatefile then
349 if updatefile then
@@ -385,13 +386,20 @@ makeLemma fn updatefile l n
385 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc
386 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc
386 appArgs skip i _ = ""
387 appArgs skip i _ = ""
388− stripMNBind _ args t | args <= 0 = t
389+ stripMNBind _ args t | args <= 0 = stripImp t
389 stripMNBind skip args (PPi b n@(UN c) _ ty sc)
390 stripMNBind skip args (PPi b n@(UN c) _ ty sc)
390 | n `notElem` skip ||
391 | n `notElem` skip ||
391 take 4 (str c) == "__pi" -- keep in type, but not in app
392 take 4 (str c) == "__pi" -- keep in type, but not in app
392− = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)
393+ = PPi b n NoFC (stripImp ty) (stripMNBind skip (args - 1) sc)
393 stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc
394 stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc
394− stripMNBind skip args t = t
395+ stripMNBind skip args t = stripImp t
397+ stripImp (PApp fc f as) = PApp fc (stripImp f) (map placeholderImp as)
399+ placeholderImp tm@(PImp _ _ _ _ _) = tm { getTm = Placeholder }
400+ placeholderImp tm = tm { getTm = stripImp (getTm tm) }
401+ stripImp (PPi b n f ty sc) = PPi b n f (stripImp ty) (stripImp sc)
396 constraints :: IState -> [Name] -> Type -> String
404 constraints :: IState -> [Name] -> Type -> String
397 constraints i [] ty = ""
405 constraints i [] ty = ""
@@ -431,12 +439,19 @@ makeLemma fn updatefile l n
431 "_aX" -> True
439 "_aX" -> True
432 _ -> False
440 _ -> False
434− guessClasses :: IState -> Context -> Term -> [Name]
442+ guessClasses :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
435− guessClasses ist ctxt (Bind n (Pi _ ty _) sc)
443+ guessClasses ist ctxt binders usednames (Bind n (Pi _ ty _) sc)
436− | isParamClass ist ty
444+ | isParamClass ist ty && any (\x -> elem x usednames)
445+ (paramNames binders ty)
437− = n : guessClasses ist ctxt sc
446+ = n : guessClasses ist ctxt (n : binders) usednames sc
438− | otherwise = guessClasses ist ctxt sc
447+ | otherwise = guessClasses ist ctxt (n : binders) usednames sc
439− guessClasses ist ctxt _ = []
448+ guessClasses ist ctxt _ _ _ = []
450+ paramNames bs ty | (P _ _ _, args) <- unApply ty
452+ where vnames [] = []
453+ vnames (V i : xs) | i < length bs = bs !! i : vnames xs
454+ vnames (_ : xs) = vnames xs
441 isClass ist t
456 isClass ist t
442 | (P _ n _, args) <- unApply t
457 | (P _ n _, args) <- unApply t