[isabelle-dev] NEWS: List comprehension

[Tobias C. Rittweiler]

Tobias Nipkow <nipkow at in.tum.de> writes:

> * HOL finally supports full list comprehensions as in Haskell, except 
> that "." is used instead of "|". As a by-product, pattern-matching 
> abstractions "% pat1 => e1 | ..." are supported as well.

I assume, `% pat1 => e1 | pat2 => e2' is equivalent to

  % a0 . case a0 of pat1 => e1 | pat2 => e2 
 
    with `a0' being a fresh identifier.

How does a multiple-arguments (automatically curried) lambda look like?

I.e. is `% pat1 pat2 ... patN => e' equivalent to

  % a0 . case a0 of 
           pat1 => % a1 . case a1 of
                            pat2 => % a2 . ...

 -T. 


-- 
Diese Nachricht wurde auf Viren und andere gefaerliche Inhalte untersucht
und ist - aktuelle Virenscanner vorausgesetzt - sauber.
Freebits E-Mail Virus Scanner