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.
By the way, you might want to use Integer
instead of Int
, since the former is unbounded and thus a better match for nat
.
Ah.. yes it should've Int
instead of int
. Thanks.
That coupled with Inlined
in the extraction command made it work.
Julin S has marked this topic as resolved.
Last updated: Feb 01 2023 at 13:03 UTC