## Stream: Coq users

### Topic: ✔ Notation error

#### Julin S (Apr 11 2022 at 05:46):

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

#### Julin S (Apr 11 2022 at 07:27):

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.

#### Notification Bot (Apr 11 2022 at 07:27):

Julin S has marked this topic as resolved.

Last updated: May 18 2024 at 10:02 UTC