equal
deleted
inserted
replaced
4719 lemma eq_Nil_null [code_unfold]: |
4719 lemma eq_Nil_null [code_unfold]: |
4720 "xs = [] \<longleftrightarrow> null xs" |
4720 "xs = [] \<longleftrightarrow> null xs" |
4721 by (simp add: null_def) |
4721 by (simp add: null_def) |
4722 |
4722 |
4723 lemma equal_Nil_null [code_unfold]: |
4723 lemma equal_Nil_null [code_unfold]: |
4724 "eq_class.eq xs [] \<longleftrightarrow> null xs" |
4724 "HOL.equal xs [] \<longleftrightarrow> null xs" |
4725 by (simp add: eq eq_Nil_null) |
4725 by (simp add: equal eq_Nil_null) |
4726 |
4726 |
4727 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where |
4727 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where |
4728 [code_post]: "maps f xs = concat (map f xs)" |
4728 [code_post]: "maps f xs = concat (map f xs)" |
4729 |
4729 |
4730 definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where |
4730 definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where |
4819 (SML "[]") |
4819 (SML "[]") |
4820 (OCaml "[]") |
4820 (OCaml "[]") |
4821 (Haskell "[]") |
4821 (Haskell "[]") |
4822 (Scala "!Nil") |
4822 (Scala "!Nil") |
4823 |
4823 |
4824 code_instance list :: eq |
4824 code_instance list :: equal |
4825 (Haskell -) |
4825 (Haskell -) |
4826 |
4826 |
4827 code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool" |
4827 code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
4828 (Haskell infixl 4 "==") |
4828 (Haskell infixl 4 "==") |
4829 |
4829 |
4830 code_reserved SML |
4830 code_reserved SML |
4831 list |
4831 list |
4832 |
4832 |