Hi.

I have a vector type in haskell (made with some extensions) like:

```
data Vector :: Nat → Type → Type
Nil :: forall a. Vector Zero a
Cons :: forall a n. a -> Vector n a -> Vector (Succ n) a
```

with values like:

```
v1 :: Vector (Succ Zero) Bool
v1 = Cons True Nil
```

Is there a way to map Coq's `Vector.t`

type to this type while extracting to haskell?

So that `v1`

can be mapped to `[true]%vector`

?

By default, extracting `Vector.t`

changes the structure a bit:

```
Example vec := [true].
Recursive Extraction vec.
(*
data T a =
Nil
| Cons a Int (T a)
vec :: T Bool
vec =
Cons True 0 Nil
*)
```

Is it possible to extract as multi-parameter type itself?

Does anyone know?

Last updated: Jun 23 2024 at 04:03 UTC