Julin S (Apr 11 2022 at 05:46): 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 _ _))).
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: Apr 20 2024 at 12:02 UTC