Stream: Coq users

Topic: Definition returning a modified vector


view this post on Zulip Julin S (Jul 18 2021 at 10:12):

I was trying to make a definition that accepts a bool vector of size n and returns the same vector with its first element removed.

So if size of input vector is n, that of the output vector would be n-1 (ignoring the edge cases like empty vector)

What should be the type of such a definition be?

This is what I started out with:

Require Import Vector.
Import Vector.VectorNotations.

Definition minus1 {n : nat} (v : Vector.t bool n) : Vector.t bool :=
  match v with
  | Vector.nil _ => []
  | Vector.cons _ _ _ _ => [1]
  end.

(I got some dummy values as return values right now)

But it gives an error saying:

In environment
n : nat
v : t bool n
The term "t bool" has type "nat -> Set" which should be Set, Prop or Type.

What am I doing wrong?

view this post on Zulip Gaëtan Gilbert (Jul 18 2021 at 10:24):

the error seems pretty clear

view this post on Zulip Ali Caglayan (Jul 18 2021 at 11:19):

Why doesn't the module appear in the error message?

view this post on Zulip Ali Caglayan (Jul 18 2021 at 11:19):

Also in case it wasn't clear enough, Vector.t bool has type nat -> Set, you still have to give it a nat to tell it how long it should be.

view this post on Zulip Ali Caglayan (Jul 18 2021 at 11:21):

There are two ways you can do this depending on what you want. You can change the start n to S n and add n to the end or keep n and use pred n.

view this post on Zulip Ali Caglayan (Jul 18 2021 at 11:21):

The former seems more sensible to me.

view this post on Zulip Gaëtan Gilbert (Jul 18 2021 at 11:21):

Ali Caglayan said:

Why doesn't the module appear in the error message?

because it's imported

view this post on Zulip Ali Caglayan (Jul 18 2021 at 11:21):

Ah I see, I missed that

view this post on Zulip Julin S (Jul 18 2021 at 12:18):

Sorry folks. I guess I got a poor Internet connection. I got your replies just now.

Thanks for the ideas!


Last updated: Feb 04 2023 at 21:02 UTC