Subject: Ssreflect Users Discussion List
List archive
- From: Thomas Sibut-Pinote <>
- To: "" <>
- Subject: big_nat_recr
- Date: Wed, 11 Apr 2012 15:52:19 +0200
Hi,
I've noticed that one cannot use big_nat_recr when there is a non trivial predicate in a sum. How does one separate the last term from the whole sum in such a case?
Thanks for your time,
Thomas
- big_nat_recr, Thomas Sibut-Pinote, 04/11/2012
- Re: big_nat_recr, bertot, 04/11/2012
Archive powered by MHonArc 2.6.18.