Stream: hs-to-coq devs & users

Topic: ✔ Error while running


view this post on Zulip Julin S (Sep 11 2022 at 16:16):

Thanks! Removing those comments made it work.

But what were the non-ASCII in those comments? I couldn't spot them.

For example, in the first line:

# Avoid module name puns, as it confuses Coqs code extraction

Which character is non-ASCII?

view this post on Zulip Karl Palmskog (Sep 11 2022 at 16:16):

the

view this post on Zulip Julin S (Sep 11 2022 at 16:23):

Oh.. got it. Thanks.

view this post on Zulip Notification Bot (Sep 11 2022 at 16:23):

Julin S has marked this topic as resolved.


Last updated: Feb 06 2023 at 05:03 UTC