When an identifier is not declared, Rodin could provide a simple way for the user to add the corresponding constant (for contexts) or variable (for machines) in a way similar to the “Quick Fixes” of the Eclipse Java editor.
Log in to post a comment.
