The Coq mailing list

[Mario Alvarez Picallo <mario.alvarez739 AT gmail.com>]

I'm sure someone has a better representation but, if you're only interested in n-bit binary numbers, you could define them inductively as:

  Inductive Unsigned : nat -> Set :=
  | Empty : Unsigned 0
  | One : forall n, Unsigned n -> Unsigned (S n)
  | Zero : forall n, Unsigned n -> Unsigned (S n)
  .

This has the advantage that it will let you write definitions and proofs by induction on the number of bits (which may or may not be what you want).

Cheers,

MAP

 

On Mon, Mar 18, 2019 at 2:11 PM <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.

--

Now I do not know whether I was then a lambda _expression_ emulating a Turing machine, or whether I am a Turing machine emulating a lambda _expression_.