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