Unable to import files from the same folder

Stream: new members

[Suryansh Shrivastava]

Are we suppose to modify our lean project in order to import files from other folder?

[Alex J. Best]

Can you be a bit more specific? How is your project set up, which version of lean are you using, and what exactly you are trying to accomplish (better yet what you already tried and doesn't work for you)