Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] Choice function in Set

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Choice function in Set


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page