-
Notifications
You must be signed in to change notification settings - Fork 11
Open
Description
In 1.6.0a1, if someone has an error in a module instantiation, for example, passing in a rule, the entire instantiation is underlined and the error message can be unspecified, e.g.
A module argument must be a syntax, judgment, rule, or theorem, but an undefined identifier was provided.
It neither underlines the argument (it underlines the entire module instantiation), nor does the message give the undefined identifier.
This appears to the case for most (all?) other module instantiation errors: the entire instantiation is underlined rather than the offending part.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels