coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Difference between sum and sumbool

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Difference between sum and sumbool
Date: Tue, 25 Aug 2015 09:51:11 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f52.google.com
Ironport-phdr: 9a23:Q+NVMhG49cribkFK4VlAUp1GYnF86YWxBRYc798ds5kLTJ75pMWwAkXT6L1XgUPTWs2DsrQf27GQ7vGrBzJIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/njKbvqtaNPU1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y5WcGIWlFJ3AgXK6BzrFN+lsCz6sPVV3iSFNNfqTKs9Xy/k5KBuHky7wBwbPiI0pTmEwvd7i7hW9Uqs
Organization: New Artisans LLC

>>>>> Dirk Pattinson
>>>>> <dirk.pattinson AT anu.edu.au>
>>>>> writes:

> Differently put: assuming I'm not interested in extraction, could I replace
> "sumbool" by "sum" throughout (assuming I would be prepared to also do this
> in the libraries)?

sum ranges over Type, so sumbool is just a fixed specialization to Prop. So
you can use sum anywhere you might use sumbool, with the noted difference that
for extraction purposes, sumbool is Bool, and sum over Prop is Either () ().

John

[Coq-Club] Difference between sum and sumbool, Dirk Pattinson, 08/25/2015
- Re: [Coq-Club] Difference between sum and sumbool, John Wiegley, 08/25/2015
  - Re: [Coq-Club] Difference between sum and sumbool, Dirk Pattinson, 08/25/2015
    - Re: [Coq-Club] Difference between sum and sumbool, Guillaume Melquiond, 08/25/2015
    - Re: [Coq-Club] Difference between sum and sumbool, John Wiegley, 08/25/2015