FStar
FStar copied to clipboard
Pretty-print basic_type_error
trafficstars
Example of after, in Pulse:
previously this was all in a single line. If it fits in the line width, it will still be in a single line, but it will break as needed. Note
but test2 is in a single line since it fits, if test2 was bigger it would also break and indent.
I removed the double quotes around the terms... should we maybe keep them? Or use anything else to distinguish terms appearing in the error message. GHC uses some fancy quotes that cannot appear in terms.
• Couldn't match expected type ‘Int’ with actual type ‘Char’