Stream: Coq users

Topic: ✔ Extraction: Haskell type constraints


view this post on Zulip Guillaume Melquiond (Aug 30 2022 at 05:52):

I don't know Haskell, so I might be wrong, but why did you use lowercase int in the first place? I am pretty sure that, if you had used Int instead, it would have worked just fine. In other words,

addC :: Int -> Int -> Int
addC = (+)

is a well-typed Haskell definition.

view this post on Zulip Guillaume Melquiond (Aug 30 2022 at 05:54):

By the way, you might want to use Integer instead of Int, since the former is unbounded and thus a better match for nat.

view this post on Zulip Julin S (Aug 30 2022 at 05:57):

Ah.. yes it should've Int instead of int. Thanks.

view this post on Zulip Julin S (Aug 30 2022 at 05:57):

That coupled with Inlined in the extraction command made it work.

view this post on Zulip Notification Bot (Aug 30 2022 at 05:58):

Julin S has marked this topic as resolved.


Last updated: Feb 01 2023 at 13:03 UTC