HomeIsabelle/Phabricator
Isabelle/ML "build" combinators

ML

  • 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.
User
Projects
None
Subscribers
None

Event Timeline