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?

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.

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: Jun 13 2024 at 04:03 UTC