UselessPrivatePragma.agda:5,1-6,28 Using private here has no effect. Private applies only to declarations that introduce new identifiers into the module, like type signatures and data, record, and module declarations.