AishwaryaSivaraman/lemmafinder

QC Example Generation with quantified hypotheses

Opened this issue · 0 comments

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.