The fact that the definition, defthm, ... forms yield runtime exceptions in case of error means that it is cumbersome to work with them at development time. In a similar way to try-proof vs proof, development time forms such as try-definition, try-defthm, ... should be added to the core functionalities.
The fact that the
definition,defthm, ... forms yield runtime exceptions in case of error means that it is cumbersome to work with them at development time. In a similar way totry-proofvsproof, development time forms such astry-definition,try-defthm, ... should be added to the core functionalities.