Julin S (Jul 18 2021 at 10:12): 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?
Gaëtan Gilbert (Jul 18 2021 at 10:24):the error seems pretty clear
Ali Caglayan (Jul 18 2021 at 11:19):Why doesn't the module appear in the error message?
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.
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.
Ali Caglayan (Jul 18 2021 at 11:21):The former seems more sensible to me.
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
Ali Caglayan (Jul 18 2021 at 11:21):Ah I see, I missed that
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: Sep 23 2023 at 07:01 UTC