Lets say I want to have something like this but for vector of arbitrary size n:

```
Inductive AllZeros : list nat -> Prop :=
| AllZeros_Empty : AllZeros []
| AllZeros_Cons (l: list nat) (n : nat): n = 0 -> AllZeros l -> AllZeros (n::l).
```

So This is the minimal error reproducer and I cannot understand the error:

```
From stdpp Require Import vector.
Inductive AllZeros {n: nat}: (vec nat n) -> Prop :=
| AllZeros_Empty : AllZeros [#].
```

The error is `cannot unify "0" and "n"`

. But this does not make sense ... it looks completely fine because in this case n will be 0.

What am I missing ?

Concretely, you want:

```
Require Import stdpp.vector.
Inductive AllZeros : ∀ {n: nat}, (vec nat n) -> Prop :=
| AllZeros_Empty : AllZeros [#].
```

binding `n`

after the equal makes it an _index_ — that is, it lets different constructors constrain `n`

, which you need here.

Binding `n`

before the `n`

, as you did, makes it a parameter (while `xs : vec nat n`

remains an index) — which means that all constructors must be able to produce `AllZeros n xs.`

for some `xs`

.

However, beware that `vector`

isn't so convenient to use in Coq. `Definition tuple A n := { xs : list A | length xs = n }.`

works better...

I have one more questions not related to coq, how do you always write those nice looking symbols ? like `∀`

I have unicode shortcuts in mac/iOS, vscode (and usually in emacs but I must reinstall them)…

https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/editor.md has extensive docs and configs — only downside is that it’s a bit focused on Iris.

Thanks, It is ok, I am planning to learn iris soon so it is upside (:

Last updated: Jun 24 2024 at 00:02 UTC