How can I declare an array type variable defined as follows:

Inductive array (n : nat) : Type :=

tab : forall l : list Z, length l = n -> array n.

I want to declare as:

arrayConstant: array

You could write `arrayConstant : array 10`

instead, for an array of length 10.

In general, yoy want `arrayConstant : array m`

for some term `m`

of type `nat`

; my last example used `m = 10`

, but that's just an example.

Thank you for your reply.

I tried to do something like this but got the error : The reference n was not found in the current environment.

With code :

Inductive array (n : nat) : Type :=

tab : forall l : list nat, length l = n -> array n.

Definition n : nat.

Inductive Const : Type :=

| arrayConstant : array n -> Const.

Is it that you want `Variable`

rather than `Definition`

? A definition has to have a body, i.e, a specific natural number in this case.

Indeed, `n`

is not available after `Definition n : nat.`

— that command just _starts_ a definition, but `n`

is only available when you've _completed_ the definition — say, after `Defined.`

eg `n`

is available after

```
Definition n : nat.
exact 42.
Defined.
```

but that is best written as

```
Definition n : nat := 42.
```

I don't need to specify a value.

I'm looking to define an array type for some semantics.

Can you say a bit more about what you're trying to do, and why neither `Definition`

nor `Variable`

is the right thing?

Do you want to say something like “a `Const`

can be an `array`

of arbitrary length”? That'd look like:

```
Inductive Const : Type :=
| arrayConst {n} : array n -> Const.
```

(with no `Definition`

or `Variable`

or whatever). The idea is that the length is another piece of data packed into the constructor `arrayConst`

(along with the actual array).

I want to define an array type.

Then use this definition as a type.

How can I make this piece of code work:

Inductive array (n : nat) : Type :=

tab : forall l : list nat, length l = n -> array n.

Inductive Const : Type :=

| arrayConstant : array -> Const.

In case it helps, you can also consider the type `{ n & array n }`

(using notation https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#e6a434cae860987d1c5f61b342cc9e57), which is what you might be thinking of when you want to use `array`

as a type (the total space of arrays). By Currying, declaring `arrayConstant : { n & array n } -> Const`

is equivalent (at the level of isomorphism) to what I gave before.

Thanks a lot.

Last updated: Jun 15 2024 at 23:01 UTC