Subject: Ssreflect Users Discussion List
List archive
- From: Florent Hivert <>
- To: Georges Gonthier <>
- Cc: "" <>
- Subject: Re: [ssreflect] Choice function in Set
- Date: Thu, 11 Feb 2016 17:36:55 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=None ; spf=None
- Ironport-phdr: 9a23:rdajBBw9cJhqe9TXCy+O+j09IxM/srCxBDY+r6Qd0eITIJqq85mqBkHD//Il1AaPBtWErakYwLqI+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStGU1Jj8h7760qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGx48sgs/M9YUKj8Y79wDfkBVGxnYCgJ45jEuB7ZQgaUrlQbVHkWkxdSS1zK6xfmXpb8qAP/t+Fn3zKdM9GwRrcxD2eM9aBuHTHsjz0KMSJx0GDJh9ZsxPZ1pBW7qhpjha7VfoyPKNJ6ZKKbc8lMFjkJZdpYSyEUWtD0VIAIFedUeL8A94Q=
Dear Georges,
On Thu, Feb 11, 2016 at 03:53:47PM +0000, Georges Gonthier wrote:
> You can easily do all this using sigW and related lemmas in choice.v, which
> convert various forms of decidable exists over choice types, to sigma types.
Thanks a lot. I completely missed it. Sorry for the stupid question.
Best,
Florent
- [ssreflect] Choice function in Set, Florent Hivert, 02/11/2016
- RE: [ssreflect] Choice function in Set, Georges Gonthier, 02/11/2016
- Re: [ssreflect] Choice function in Set, Florent Hivert, 02/11/2016
- Re: [ssreflect] trivIset and intersecting sets..., Florent Hivert, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Beta Ziliani, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Emilio Jesús Gallego Arias, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Emilio Jesús Gallego Arias, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Emilio Jesús Gallego Arias, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Florent Hivert, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Emilio Jesús Gallego Arias, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Emilio Jesús Gallego Arias, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Florent Hivert, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Emilio Jesús Gallego Arias, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Emilio Jesús Gallego Arias, 02/12/2016
- Re: [ssreflect] trivIset and intersecting sets..., Assia Mahboubi, 02/21/2016
- RE: [ssreflect] Choice function in Set, Georges Gonthier, 02/11/2016
Archive powered by MHonArc 2.6.18.