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 <leegys AT gmail.com>
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:38:26 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type; b=YoU2amb5LraF3BGohTT3xYwfpVFXgpG6jJM5K8P88N0Q344ribQ7bRG99Kzt9fem0H l/52sCQ3SeLw8AJItCAetRqDwlqIPjsSXLhFEqpA8BqWcuVaplafGKt8p3AHMQcnUO9u Ag72cJr7JMyTVwFHd1J8hUlRZyMM5mNLMzZp0=

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