Elab type before value in definitions.
Elab type before value in definitions.

This isn't a big deal, you just kinda expect to see a type elaboration
error (due to needing an annotation) before a value elaboration error.

spire/spire