Re: [isabelle] Isabelle Cookbook example



On Wed, 15 Sep 2010, Steve W wrote:

Could you tell me where '--' and the '>>' infix operators are implemented?

Most of this is in src/Pure/General/scan.ML -- the only non-conventional extension of well-established ideas of combinator parsing is support for potentially infinite input.

Many textbooks on functional programming explain the general idea, e.g. Larry's ML book. In the end only some notational details differ, i.e. the names of the usual cominators, such as "--" for pairing and ">>" for mapping of results.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.