Stream: Coq users

Topic: QuickChick - Not Checkable


view this post on Zulip Mohammad-Ali A'RÂBI (Apr 26 2021 at 22:54):

Hello, people. I followed the QuickChick tutorial (from its GitHub code) and ended up here:
https://github.com/aerabi/lttt/blob/master/src/QuickChick.v
But when I add QuickChick 𝔱_preservation_fun., I get the following error:

Unable to satisfy the following constraints:

?arg_2 : "Checkable (m𝔊.T -> 𝔱 -> 𝔱 -> 𝔗 -> Prop)"

Any ideas on what could it be?

view this post on Zulip Zoe Paraskevopoulou (Apr 27 2021 at 10:27):

Hi there, this means the typeclass resolution is unable to find a Checkable instance for one of your inductive predicates. Adding decidability (Dec) instances for your type𝔗, 𝔱sem should do the trick. You also need to make sure that you have Arbitrary instances for your inputs to check this property.

view this post on Zulip Mohammad-Ali A'RÂBI (May 11 2021 at 09:39):

Thanks a lot, @Zoe Paraskevopoulou. After doing the suggested solutions, I learned that Coq cannot infer Checkable instances for my types, as they are mutually inductive. Do you have any suggestions? Thanks again.


Last updated: Jan 29 2023 at 06:02 UTC