Matthieu Sozeau (Jan 17 2021 at 18:15): Matthieu Sozeau (Jan 17 2021 at 18:15):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: Apr 16 2024 at 10:01 UTC