module Core.InitPrimitives import Core.Contextimport Core.Primitivesimport Core.TT -- import Data.NameMap %default covering addPrim : {auto c : Ref Ctxt Defs} ->          Prim -> Core ()addPrim p    = do addBuiltin (opName (fn p)) (type p) (totality p) (fn p)         -- compileDef empty (opName (fn p)) exportaddPrimitives : {auto c : Ref Ctxt Defs} -> Core ()addPrimitives    = traverse_ addPrim allPrimitives