Right now elaboration halts on the first error. We will probably have to continue doing that while elaborating a single declaration (for now), but elaborating a whole module could collect the errors from multiple declarations in a single pass.
Same thing applies to renaming, and possibly module imports (we could check the whole module graph at once).
Right now elaboration halts on the first error. We will probably have to continue doing that while elaborating a single declaration (for now), but elaborating a whole module could collect the errors from multiple declarations in a single pass.
Same thing applies to renaming, and possibly module imports (we could check the whole module graph at once).