I made a heterogenous list (hlist) like:

```
Require Import List.
Import ListNotations.
Inductive hlist (A : Type) (B : A -> Type) : list A -> Type :=
| hnil : hlist A B []
| hcons : forall (x : A) (ls : list A),
(B x) -> hlist A B ls -> hlist A B (x::ls).
```

I didn't make any argument implicit yet.

I can make hlists like:

```
Example hls1 : hlist Set (fun x => x) [nat; bool] :=
hcons Set (fun x=>x) nat [bool] 3
(hcons Set (fun x=>x) bool [] true (hnil _ _)).
Example hls2 : hlist Set (fun x => x) [bool; nat; bool] :=
hcons Set (fun x=>x) bool[nat;bool] false
(hcons Set (fun x=>x) nat [bool] 3
(hcons Set (fun x=>x) bool [] true (hnil _ _))).
```

Then I tried making a function to append to hlists and did:

```
Fixpoint happ {A:Type} {B:A->Type} {ls1 ls2: list A}
(hls1 : hlist A B ls1) (hls2: hlist A B ls2) :
hlist A B (ls1++ls2)%list :=
match hls1 in (hlist _ _ ls1) return
hlist A B (ls1++ls2)%list with
| hnil _ _ => hls2
| hcons _ _ _ _ y ys =>
hcons A B _ (tail (ls1++ls2)) y (happ ys hls2)
(*| hcons _ _ _ _ y ys => hcons A B (head ls1) (tail (ls1++ls2)) y (happ ys hls2) *)
end.
```

But that's giving error:

```
In environment
happ : forall (A : Type) (B : A -> Type) (ls1 ls2 : list A),
hlist A B ls1 -> hlist A B ls2 -> hlist A B (ls1 ++ ls2)
A : Type
B : A -> Type
ls1 : list A
ls2 : list A
hls1 : hlist A B ls1
hls2 : hlist A B ls2
a : A
l : list A
y : B a
ys : hlist A B l
The term "happ A B l ls2 ys hls2" has type "hlist A B (l ++ ls2)"
while it is expected to have type "hlist A B (List.tl (ls1 ++
ls2))".
```

I'm guessing that I was not able to let coq figure out that the `(l ++ ls2)`

is

same as the `(List.tl (ls1 ++ ls2))`

.

Had a similar problem earlier which was fixed (with help from here) by using

`return`

in `match`

statement. Can this also be fixed similarly?

Put `_`

instead of `tail (ls1 ++ ls2)`

.

Or get the tail of `ls1`

from the `hcons`

pattern (which the error message names `l`

).

Thanks, that made it right.

Last updated: Jun 13 2024 at 04:03 UTC