Hello, people. I followed the QuickChick tutorial (from its GitHub code) and ended up here:
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?
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
𝔱sem should do the trick. You also need to make sure that you have
Arbitrary instances for your inputs to check this property.
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