Mohammad-Ali A'RÂBI (Apr 26 2021 at 22:54): 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?
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.
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: Oct 13 2024 at 01:02 UTC