Stream: Coq users

Topic: Notation levels for abbreviation

view this post on Zulip 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: Feb 01 2023 at 11:04 UTC