Re: [isabelle] Isabelle Cookbook example





Makarius writes:
 > 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.

Hi Steve,

These combinators are also explained with examples in the
parsing chapter of the Isabelle programming tutorial.

Hope this helps,
Christian





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