at the moment, all code that is typechecked has to be inside a module. hence, individual files cannot be checked if they don't define a module. on the other hand, if they do defne a module they cannot be used with include in other files that are supposed to be checked, because that would lead to a nested module inside the including module and we don;t allow using stuff from modules inside tyecheckable code. might be handy to implement this but seems a bit involved.
at the moment, all code that is typechecked has to be inside a module. hence, individual files cannot be checked if they don't define a module. on the other hand, if they do defne a module they cannot be used with
includein other files that are supposed to be checked, because that would lead to a nested module inside the including module and we don;t allow using stuff from modules inside tyecheckable code. might be handy to implement this but seems a bit involved.