on master help sign in
Minor tweak to metavariable type generation
84ba376Edwin Brady
src/Idris/Elab/Term.hs+4
@@ -1573,6 +1573,10 @@ collectDeferred top ctxt (Bind n (GHole i t) app) =
1573 tidy ctxt env t | (f, args) <- unApply t,
1573 tidy ctxt env t | (f, args) <- unApply t,
1574 P _ n _ <- getFn f
1574 P _ n _ <- getFn f
1575 = fst $ specialise ctxt env [(n, 99999)] t
1575 = fst $ specialise ctxt env [(n, 99999)] t
1576+ tidy ctxt env t@(Bind n (Let _ _) sct)
1577+ | (f, args) <- unApply sct,
1578+ P _ n _ <- getFn f
1579+ = fst $ specialise ctxt env [(n, 99999)] t
1576 tidy ctxt env t = t
1580 tidy ctxt env t = t
1577
1581
1578 getFn (Bind n (Lam _) t) = getFn t
1582 getFn (Bind n (Lam _) t) = getFn t