If we have
datatype 'a foo = Foo 'a | Goo
notation_nano_rust_function foo.Foo ("Foo::Foo")
notation_nano_rust foo.Goo ("Foo::Goo")
then the notation for foo.Foo does not get registered properly and leads to type errors when trying to use the pattern Foo::Foo(x) in the arm of a match. Instead, we have to do the following dance:
notation_nano_rust foo.Foo ("Foo::FooM")
notation_nano_rust foo.Goo ("Foo::Goo")
abbreviation ‹foo_foo_urust ≡ lift_fun1 Foo›
notation_nano_rust_function foo_foo_urust ("Foo::Foo")
to make this work.