Double Error message when improperly using string in a theory

The given file uses a string in the theory, but the type where the string is used is not a subtype of string. This is incorrect code and indeed an error message is shown when running the file. The bug is that the error message is generated twice.

[joachim@yonder] [~/documents/theories/bugtests]$ idp bug_parse_double_error_message.idp 
Error: Term 0 has sort string but occurs in a position with sort T. At bug_parse_double_error_message.idp:11:7
Error: Term 0 has sort string but occurs in a position with sort T. At bug_parse_double_error_message.idp:11:7

Comments (2)