Robert Soeldner (Jun 04 2021 at 18:57): Robert Soeldner (Jun 04 2021 at 18:57):Does Isabelle offer some equivalent to Haskell's as-pattern https://en.wikibooks.org/wiki/Haskell/Pattern_matching#As-patterns ?
Lukas Stevens (Jun 04 2021 at 18:59):Yes, ~~/src/HOL/Library/Pattern_Aliases.thy.
Robert Soeldner (Jun 04 2021 at 19:02):Thank you :) Is there some nice page where I can scroll through to get a better understanding of what is available ?
Lukas Stevens (Jun 04 2021 at 19:04):Not really. You can look at this document to see what is in the Library: https://isabelle.in.tum.de/library/HOL/HOL-Library/document.pdf
Manuel Eberl (Jun 04 2021 at 19:57):There is the "What's in main" document on the website/in the documentation that lists some of the stuff that is in HOL. But nothing like that exists for HOL-Library. I would just have a look through it once.
Last updated: Apr 23 2024 at 08:19 UTC