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