Ambiguous notations for vectors and telescopes
From stdpp Require Import telescopes list.
Check [ tele ]. (* prints [tele] : list Type *)
Check [tele]. (* prints [tele] : tele *)
This is due to the notations in https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/telescopes.v?ref_type=heads#L167
Notation "'[tele' ]" := (TeleO)
(format "[tele ]").
This shows that [ tele ]
is parsed as a list, but it pretty prints without space, i.e., [tele]
. When parsing this again, we end up with the empty telescopes.
See @snyke7's post below for a similar issue for vectors.
Edited by Robbert Krebbers