git.iko.soy/Idris-dev
on master help sign in
Allow resolving metavariables from ibcs
4e0bdc8Edwin Brady
src/Idris/IBC.hs+5−2
compare with master
unifiedsplit
@@ -400,8 +400,11 @@ pPatdefs ds
400pDefs :: [Name] -> [(Name, Def)] -> Idris ()
400pDefs :: [Name] -> [(Name, Def)] -> Idris ()
401pDefs syms ds
401pDefs syms ds
402 = mapM_ (\ (n, d) ->
402 = mapM_ (\ (n, d) ->
403− do i <- getIState
404− let d' = updateDef d
403+ do let d' = updateDef d
404+ case d' of
405+ TyDecl _ _ -> return ()
406+ _ -> solveDeferred n
407+ i <- getIState
405 logLvl 5 $ "Added " ++ show (n, d')
408 logLvl 5 $ "Added " ++ show (n, d')
406 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds
409 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds
407 where
410 where