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: Nov 21 2024 at 12:39 UTC