Is a generic version of
'a set set => 'a set available? Currently I apply
image to a set with a function returning a set.
term "⋃" (* "⋃" :: "'a set set ⇒ 'a set" *)
(\<Union>, Un for typing)
in Query > finding constants, you can type
‹'a set set ⇒ 'a set› and find that:
find_consts "'a set set ⇒ 'a set" found 2 constant(s): Complete_Lattices.Inter :: "'a set set ⇒ 'a set" Complete_Lattices.Union :: "'a set set ⇒ 'a set"
thank you, is there something like hoogle for Isabelle?
Ha, thank you! :tada:
As far as I know, neither SErAPIS nor https://search.isabelle.in.tum.de/ support searching for a type.
Last updated: Jul 15 2022 at 23:21 UTC