QC Example Generation with quantified hypotheses
Opened this issue · 0 comments
AishwaryaSivaraman commented
If a goal state contains a hypothesis that is quantified, for example, due to intros not being used before induction, then quickchick might not generate examples.
lfind
allows the processing of such goal states, if the examples are manually provided, otherwise, it exits.
We may need to investigate more about this issue, i.e. if QC is able to generate examples, if not, is there anything that we can do to automate the generation.