[isabelle-dev] NEWS: Isabelle/ML "build" combinators
makarius at sketis.net
Wed Sep 22 12:39:18 CEST 2021
*** ML ***
* The "build" combinators of various data structures help to build
content from bottom-up, by applying an "add" function the "empty" value.
- type 'a Symtab.table etc.: build
- type 'a Names.table etc.: build
- type 'a list: build and build_rev
- type Buffer.T: build and build_content
For example, see src/Pure/PIDE/xml.ML:
val content_of = Buffer.build_content o fold add_content;
This refers to Isabelle/4974c3697fee.
It may be seen as the final capstone for our approach to "canonical argument
order": it has turned out very beneficial to Isabelle/ML readability and
conciseness since 2005 (especially in contrast to the monadic bloat seen in
We did not have "build" combinators in the past, because most applications
were for plain lists where "empty" is just . For other data structures, it
does help to make the point more clear.
More information about the isabelle-dev