FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Pretty-print basic_type_error

Open mtzguido opened this issue 2 years ago • 0 comments
trafficstars

Example of after, in Pulse: Screenshot 2023-09-29 111721 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’

mtzguido avatar Sep 29 '23 18:09 mtzguido