on master help sign in
No need to export primitives as metavariables

...they just clutter the display.

commit7b32c970e85082334dbd38659318287969629e2b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 28 Feb 2014, 09:46 (13 years ago) parent2df0a7f
1 file changed+1−1
src/Idris/AbsSyntax.hs+1−1
src/Idris/AbsSyntax.hs+1−1
@@ -460,7 +460,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)
460460addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
461461addDeferred' nt ns
462462 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
463− mapM_ (\(n, _) -> addIBC (IBCMetavar n)) ns
463+ mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
464464 i <- getIState
465465 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
466466 idris_metavars i }