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