'\0' is translated to incorrect f*

[maximebuyse]

The rust character '\0' is translated as '\000' in f* which is rejected with unexpected char by f*.
Writing 0x00 as char works as a workaround.

[W95Psp]

Oh, it seems that it's a bug in the pretty printer of F*

[W95Psp]

I opened FStarLang/FStar#3560 on F*. But this will likely be fixed by #942: with that, we won't use F* pretty printer anymore.

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

This was closed by #1147