coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
- To: Fred Smith <fsmith1024 AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proof irrelevant Specif?
- Date: Sat, 28 May 2016 10:57:54 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT boipeva.ensmp.fr
- Ironport-phdr: 9a23:SfaCcxyUFlI0YoPXCy+O+j09IxM/srCxBDY+r6Qd0eIQIJqq85mqBkHD//Il1AaPBtWKra8cwLKG+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt+U0pz8j7D60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGx48sgs/M9YUKj8Y79wDfkBVGxnYCgJ45jFrxTPBTCK52ccGjEYiR9JHwictEumdpj0uyr+8OF63X/JE9fxSOU5Gj+l9uJgTALioDdXb3g+6m6fyuF1jaZap1qDqgft2Mb7aYWROfV5NorHfNoBBDkSFv1NXjBMV9vvJ7AECPAMaKMB99Hw
- Organization: X80 Heavy Industries
Fred Smith
<fsmith1024 AT gmail.com>
writes:
> I wanted to define a small range of numbers and thought this would be a
> clean solution:
By the way, ordinals (Fin.t or 'I_n in mathcomp) provide exactly an
already-built solution for this use case.
'I_n is indeed defined as:
'I_n := { x : nat | x < n }
and math-comp provides an extensive theory about them, see:
http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.fintype.html
Best regards,
E.
- [Coq-Club] Proof irrelevant Specif?, Fred Smith, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Robbert Krebbers, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Emilio Jesús Gallego Arias, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Emilio Jesús Gallego Arias, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Fred Smith, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Emilio Jesús Gallego Arias, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Fred Smith, 05/28/2016
Archive powered by MHonArc 2.6.18.