Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Isabelle/ML "build" combinators

view this post on Zulip Email Gateway (Sep 22 2021 at 10:39):

From: Makarius <>
* ML *

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
Haskell libraries).

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.


isabelle-dev mailing list

Last updated: Mar 04 2024 at 12:30 UTC