# HG changeset patch # User wenzelm # Date 1301348993 -7200 # Node ID 15218eb98fd711e710fb13c6ea208ce674d8f915 # Parent 786ccfffcd67f8b4ef98ba2af345ee6b0020989b list comprehension: strip positions where the translation cannot handle them right now; diff -r 786ccfffcd67 -r 15218eb98fd7 src/HOL/List.thy --- a/src/HOL/List.thy Mon Mar 28 22:44:14 2011 +0200 +++ b/src/HOL/List.thy Mon Mar 28 23:49:53 2011 +0200 @@ -341,16 +341,17 @@ mangled). In such cases it can be advisable to introduce separate definitions for the list comprehensions in question. *} -nonterminal lc_qual and lc_quals +nonterminal lc_gen and lc_qual and lc_quals syntax "_listcompr" :: "'a \ lc_qual \ lc_quals \ 'a list" ("[_ . __") -"_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ <- _") +"_lc_gen" :: "lc_gen \ 'a list \ lc_qual" ("_ <- _") "_lc_test" :: "bool \ lc_qual" ("_") (*"_lc_let" :: "letbinds => lc_qual" ("let _")*) "_lc_end" :: "lc_quals" ("]") "_lc_quals" :: "lc_qual \ lc_quals \ lc_quals" (", __") "_lc_abs" :: "'a => 'b list => 'b list" +"_strip_positions" :: "'a \ lc_gen" ("_") (* These are easier than ML code but cannot express the optimized translation of [e. p<-xs] @@ -366,9 +367,9 @@ *) syntax (xsymbols) -"_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ \ _") +"_lc_gen" :: "lc_gen \ 'a list \ lc_qual" ("_ \ _") syntax (HTML output) -"_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ \ _") +"_lc_gen" :: "lc_gen \ 'a list \ lc_qual" ("_ \ _") parse_translation (advanced) {* let