Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Prefix notation without parenthesis


view this post on Zulip Email Gateway (Aug 22 2022 at 21:13):

From: Joshua Morris <joshuajohnmorris@gmail.com>
I have a function lib_first :: "'b ⇒ 'a::complete_distrib_lattice ⇒ 'a" and
want to be able to use prefix notation that looks like "F⇧C _ _". If I do
lib_first :: "'b ⇒ 'a::complete_distrib_lattice ⇒ 'a" ("F⇧C _ _" [10] 10)
then I get the desired result except that every instance must be surrounded
by parenthesis. Is there a way I can do something like this without having
to use parenthesis for every instance?


Last updated: Mar 28 2024 at 08:18 UTC