Stream: Beginner Questions

Topic: Generic 'a set set => 'a set

Robert Soeldner (Apr 24 2021 at 18:24):

Is a generic version of 'a set set => 'a set available? Currently I apply image to a set with a function returning a set.

Mathias Fleury (Apr 24 2021 at 18:27):

term "⋃"
(* "⋃"
  :: "'a set set ⇒ 'a set" *)

(\<Union>, Un for typing)

Mathias Fleury (Apr 24 2021 at 18:28):

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"

Robert Soeldner (Apr 24 2021 at 18:28):

thank you, is there something like hoogle for Isabelle?

Robert Soeldner (Apr 24 2021 at 18:28):

Ha, thank you! :tada:

Mathias Fleury (Apr 24 2021 at 18:32):

As far as I know, neither SErAPIS nor https://search.isabelle.in.tum.de/ support searching for a type.

Last updated: Dec 21 2024 at 16:20 UTC