Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Lists over a set

view this post on Zulip Email Gateway (Aug 19 2022 at 07:58):

From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Quick question:

Is there an existing Isabelle theory for lists whose elements are
members of a given set? I.e. a theory for lists over a given set?

Thanks,
Stephan

view this post on Zulip Email Gateway (Aug 19 2022 at 07:58):

From: Tobias Nipkow <nipkow@in.tum.de>
Yes, in theory List there is a function lists :: 'a set => 'a list set

The document "What's in Main" http://isabelle.in.tum.de/documentation.html may
also be helpful to find your way around the predefined concepts.

Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 07:58):

From: Peter Lammich <lammich@in.tum.de>
Try List.lists :: 'a set => 'a list set

Peter

view this post on Zulip Email Gateway (Aug 19 2022 at 07:58):

From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Great, thanks for the quick reply.

Last updated: Apr 20 2024 at 04:19 UTC