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).
```

For this, I tried making notations in the style of the notations for `List.list`

like:

```
Notation "[[ ]]" := (hnil _ _)
(at level 60).
Notation "[[ x ]]" := (hcons Set (fun x=>x) _ _ x (hnil _ _))
(at level 55, x constr at next level).
(*
Notation "[[ x , y , .. , z ]]" :=
(hcons Set (fun x=>x) _ _ x
(hcons Set (fun x=>x) _ _ y ..
(hcons Set (fun x=>x) _ _ z
(hnil _ _)) .. )).
*)
```

These two notation declarations got executed all right. And the usage of the first one works too.

```
Check [[]].
(*
[[ ]]
: hlist ?A ?B []
where
?A : [ |- Type]
?B : [ |- ?A -> Type]
*)
```

But when I try using the second notation, I get error:

```
Check [[ 3 ]].
(*
This expression should be a name.
*)
```

Why could this be happening?

I am able to 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 _ _))).
```

Heh heh, it's a mistake that I made.

I figured out the problem.

In

```
Notation "[[ x ]]" := (hcons Set (fun x=>x) _ _ x (hnil _ _))
(at level 55, x constr at next level).
```

the `x`

in `fun x=>x`

needed to be changed to another name.

Thanks.

Julin S has marked this topic as resolved.

Last updated: Dec 05 2023 at 12:01 UTC