The Coq mailing list

[Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>]

For the finite type of numbers `0,...,n-1` there already is `Fin.t n` in
Coq's standard library. [1]
It is a classical example for a dependent inductive type.
However, this type can be quite tricky for beginners.

I have heard of implementations of machine integers (like unsigned 8),
but I currently don't have a link.


For general *finite types*, you can do something like

```
Require Import List.

Class finite (X:Type) :=
  {
    enum : list X;
    enum_complete : forall (x:X), In x enum;
  }.

Instance finite_unit : finite unit :=
  {| enum := cons tt nil |}.
Proof. abstract now intros []; constructor. Defined.
```


[1] https://coq.inria.fr/distrib/current/stdlib/Coq.Vectors.Fin.html


Sincerely
Maximilian


On 18/03/2019 15:10, 
fritjof AT uni-bremen.de
 wrote:
> Hi,
> 
> I want to create a finite data type, like *Unsinged 8*,
> which containes values from 0 to 2^8 -1.
> I came up with an idea like:
> 
> Definition unsigned (max:Z) : Set :=
>   { x : Z | x >= 0 /\ x < max}.
> 
> Definition unsigned_8 := unsigned (2^8).
> 
> But I'm not sure, if this is the right way.
> 
> Does someone know if there is a better way to define
> finite types?
> 
> --f.
>

Attachment: signature.asc
Description: OpenPGP digital signature