Stream: Coq users

Topic: ✔ Notation error


view this post on Zulip 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 _ _))).

view this post on Zulip 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.

view this post on Zulip Notification Bot (Apr 11 2022 at 07:27):

Julin S has marked this topic as resolved.


Last updated: Jan 31 2023 at 14:03 UTC