The Coq mailing list

[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