The Coq mailing list

[Gyesik Lee <leegys AT gmail.com>]

Many thanks to all for valuable suggestions.
At a first glance, Thomas' suggestion seems very simple and intuitive for me.
(indeed it corresponds to the standard definition of finiteness in set 
theory.)
What I need is just an assumption of a finite set of symbols and not a
theory on it.
In this sense, I am not sure if I need the standard libraries such as
FSets (or MSets).

Gyesik



2011/5/6 Thomas Strathmann 
<thomas AT pdp7.org>:
> On 5/6/11 10:38 , Gyesik Lee wrote:
>>
>> 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.
>
> You can do the latter in Coq by defining an inductive type of natural
> numbers less than n that you can use in much the same way as you would
> [nat].
>
> Inductive fin : nat -> Type :=
> | FO : forall n, fin (S n)
> | FS : forall n, fin n -> fin (S n).
> Implicit Arguments FO [n].
> Implicit Arguments FS [n].
>
>        Thomas
>