checkTotalityOK : Ref Ctxt Defs => Name -> Core (Maybe Error)
getTotalityErrors : Ref Ctxt Defs => Core (List Error)