coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] how to represent the assumption of a finite set

From: Gyesik Lee <gslee AT hknu.ac.kr>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] how to represent the assumption of a finite set
Date: Fri, 6 May 2011 17:24:00 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=MF/8Z3MLQ/a3kS+cDXP3Gm3LPkL7mp/cOeNVUUl4FuOrrXXDl/of8TCgOPgspBK6PV 1OUOF95NuE1xz1six0UlZFC0l8HNxQ3ZLqbAJuy/SdCa6Fq6W+sIGUTwbQVLeXS1fLD+ xrSDXRCgpA3/b0h13rF+m0JDr5T2idiD8uDcU=

Hi,

many languages are based on a finite set of symbols.
I am wondering how to represent phrases such as "Let L be a finite set
of constants".
On paper, we usually say, L is indexed by numbers less than a natural number.
Is there a simple, intuitive way to do the same thing in Coq?
Any help will be appreciated.

Gyesik

[Coq-Club] how to represent the assumption of a finite set, Gyesik Lee
- <Possible follow-ups>
- [Coq-Club] how to represent the assumption of a finite set, Gyesik Lee
  - Re: [Coq-Club] how to represent the assumption of a finite set, Vincent
    - Re: [Coq-Club] how to represent the assumption of a finite set, Damien Pous
    - Re: [Coq-Club] how to represent the assumption of a finite set, Damien Pous
      - Re: [Coq-Club] how to represent the assumption of a finite set, Alexandre Pilkiewicz
        
        Re: [Coq-Club] how to represent the assumption of a finite set, AUGER Cedric
  - Re: [Coq-Club] how to represent the assumption of a finite set, Thomas Strathmann
    - Re: [Coq-Club] how to represent the assumption of a finite set, Gyesik Lee