equal
deleted
inserted
replaced
254 "_lc_test" :: "bool \<Rightarrow> lc_qual \<Rightarrow> lc_qual" (",__") |
254 "_lc_test" :: "bool \<Rightarrow> lc_qual \<Rightarrow> lc_qual" (",__") |
255 |
255 |
256 |
256 |
257 translations |
257 translations |
258 "[e. p\<leftarrow>xs]" => "map (%p. e) xs" |
258 "[e. p\<leftarrow>xs]" => "map (%p. e) xs" |
259 "_listcompr e p xs (_lc_gen q ys GT)" => |
259 "_listcompr e p xs (_lc_gen q ys Q)" => |
260 "concat (map (%p. _listcompr e q ys GT) xs)" |
260 "concat (map (%p. _listcompr e q ys Q) xs)" |
261 "_listcompr e p xs (_lc_test P GT)" => "_listcompr e p (filter (%p. P) xs) GT" |
261 "_listcompr e p xs (_lc_test P Q)" => "_listcompr e p (filter (%p. P) xs) Q" |
262 |
262 |
263 (* Some examples: |
263 (* Some examples: |
264 term "[(x,y). x \<leftarrow> xs, x<y]" |
264 term "[(x,y). x \<leftarrow> xs, x<y]" |
265 term "[(x,y). x \<leftarrow> xs, x<y, z\<leftarrow>zs]" |
265 term "[(x,y). x \<leftarrow> xs, x<y, z\<leftarrow>zs]" |
266 term "[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x<y]" |
266 term "[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x<y]" |