Ssreflect Users Discussion List

[Florent Hivert <>]

      Hi There,

I hope I'm not asking a question as stupid as my last one...

One great benefit of boolean reflection when trying to prove combinatorics is
that, Coq is able to automatically decide the truth of many particular cases
which are omnipresent in there. My experience is that it is quite helpful
here. However when playing with finset, I can't manage to compute
anything... Here is an example. There is only one partition of the empty set,
the empty set itself.

Lemma blu : [set p | partition p [set: 'I_0]] == [set set0].
Proof.
  compute.

Ten minutes later I stopped Coq which has exhausted the 32GB of memory of my
computer. Is this expected ? Is there a workaround ?

Best regards,

Florent