Stream: Beginner Questions

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


view this post on Zulip 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.

view this post on Zulip Mathias Fleury (Apr 24 2021 at 18:27):

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

(\<Union>, Un for typing)

view this post on Zulip 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"

view this post on Zulip Robert Soeldner (Apr 24 2021 at 18:28):

thank you, is there something like hoogle for Isabelle?

view this post on Zulip Robert Soeldner (Apr 24 2021 at 18:28):

Ha, thank you! :tada:

view this post on Zulip 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: Jul 15 2022 at 23:21 UTC