We have some lonely notations
The following is the list of notations that are "lonely", which means they are not in a scope: (in some heap_lang file, so there might be things this does not import)
Lonely notations
"✓{ n } x" := validN n x
"◯V a" := view_frag a
"◯ a" := auth_frag a
"●{ q } a" := auth_auth q a
"●V{ q } a" := view_auth q a
"●V a" := view_auth (pos_to_Qp xH) a
"● a" := auth_auth (pos_to_Qp xH) a
"↑ x" := up_close x
"'λne' x .. y , t" := OfeMor (fun x => .. (OfeMor (fun y => t)) ..)
"'λ' x .. y , t" := fun x => .. (fun y => t) ..
"x ◎ y" := ccompose x y
"x ≥ y" := ge x y
"x ≤ y" := le x y
"x ≡{ n }≡ y" := dist n x y
"x ≡{ n }@{ A }≡ y" := dist n x y
"x ~~>: y" := cmra_updateP x y
"x ~~> y" := cmra_update x y
"x ~l~> y" := local_update x y
"x ||* y" := zip_with orb x y
"x =.>* y" := Forall2 bool_le x y
"x =.> y" := bool_le x y
"x :b: y" := cons_binder x y
"p .2" := snd p
"p .1" := fst p
"ps .*2" := fmap snd ps
"ps .*1" := fmap fst ps
"TT -t> A" := tele_fun TT A
"A -n> B" := ofe_morO A B
"A -d> B" := discrete_funO (fun _ => B)
"x +b+ y" := app_binder x y
"x &&* y" := zip_with andb x y
"'[tele_arg' x ; .. ; z ]" := TargS x .. (TargS z TargO) ..
"'[tele_arg' ]" := TargO
"'[tele' x .. z ]" := TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)
"'[tele' ]" := TeleO
"(||)" := orb
" () " := tt
"(&&)" := andb
"( H 'with' pat )" := {| itrm := H; itrm_vars := hlist.hnil; itrm_hyps := pat |}
"( H $! x1 .. xn 'with' pat )" := {|
itrm := H;
itrm_vars := hlist.hcons x1 .. (hlist.hcons xn hlist.hnil) ..;
itrm_hyps := pat |}
"( H $! x1 .. xn )" := {|
itrm := H;
itrm_vars := hlist.hcons x1 .. (hlist.hcons xn hlist.hnil) ..;
itrm_hyps := EmptyString |}
"#[ Σ1 ; .. ; Σn ]" := gFunctors.app Σ1 .. (gFunctors.app Σn gFunctors.nil) ..
"#[ ]" := gFunctors.nil
"# l" := LitV l
Many of those are from Iris or std++, and are probably oversights.