Isabelle/ML "build" combinators
- The build combinators of various data structures help to build content from bottom-up, by applying an add function the empty value. For example:
- 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.
Written by makarius on Sep 22 2021, 12:11 PM.