Hi. I was trying to make a 'custom' boolean vector type which uses the built-in `Vector.t`

type.

A type `boolvector`

that takes a length argument of type `nat`

.

So I did:

```
Require Vector.
Import Vector.VectorNotations.
Inductive type : Type :=
| boolvector: nat -> type.
Definition typeDenote (t: type) : Type :=
match t with
| boolvector n => Vector.t bool n
end.
```

But I couldn't figure how to make a definition which accepts arguments of this `boolvector`

as argument.

I tried

```
Definition def1 (a: boolvector) : nat :=
match a with
| boolvector x => x
end.
```

but got this error.

```
= Vector.t bool 2
: Type
```

Can you help me find what I am doing wrong here?

EDIT: Sorry the error message above is not the real one. The actual error was

```
The term "boolvector" has type "nat -> type"
which should be Set, Prop or Type.
```

This is very confusing. For instance the "error" you showed is not an error (note how it doesn't say "error") and is not produced by any of the code you gave.

Please explain in more detail what your goal is and how you tried to reach it.

```
Inductive type : Type :=
| boolvector: nat -> type.
```

is creating a new type called `type`

which is inhabited by `boolvector n`

for each natural number `n`

.

So you are essentially creating a copy of natural numbers except that they are boxed. I don't think that's what you want to do.

Wouldn't you rather want to have the following?

```
Definition boolvector n := Vector.t bool n.
```

@Gaëtan Gilbert Oops.. Sorry that was a mistake. The real error message was:

```
The term "boolvector" has type "nat -> type"
which should be Set, Prop or Type.
```

Théo Winterhalter said:

`Inductive type : Type := | boolvector: nat -> type.`

is creating a new type called

`type`

which is inhabited by`boolvector n`

for each natural number`n`

.

So you are essentially creating a copy of natural numbers except that they are boxed. I don't think that's what you want to do.

What I meant to do was to create a `boolvector`

type for every natural number. Like `boolvector 1`

for a vector of size 1, `boolvector 2`

for a vector of size 2, etc.

And I also wanted to add more constructors for `type`

later. That's why I made it like that.

Yes, but you're not creating a type that way. `boolvector n`

is not a type with your definition. It is with mine.

And that's what the error message is telling you.

Théo Winterhalter said:

Yes, but you're not creating a type that way.

`boolvector n`

is not a type with your definition. It is with mine.

Maybe I need to something with the `typeDenote`

for that? To do some translation to `Type`

?

(Was reading CDPT book by Adam Chlipala :-D )

Last updated: May 18 2024 at 08:40 UTC