I'd like to have a notation `fn := t`

to be parsed just like an abbreviation `Notation fn := t`

but I can't find the right level annotations so that `fn x`

is parenthesized correctly at printing time (note how I "apply" the notation). So I'm wondering, is it possible to do so? Otherwise, I'm doing this to workaround the limination of `Inductive ... where notation_decl`

which doesn't accept notation declarations for abbreviations, I guess it would be easy to fix that instead.

Last updated: Sep 26 2023 at 11:01 UTC