equal
deleted
inserted
replaced
97 lemma is_none_none: |
97 lemma is_none_none: |
98 "is_none x \<longleftrightarrow> x = None" |
98 "is_none x \<longleftrightarrow> x = None" |
99 by (simp add: is_none_def) |
99 by (simp add: is_none_def) |
100 |
100 |
101 lemma [code_unfold]: |
101 lemma [code_unfold]: |
102 "eq_class.eq x None \<longleftrightarrow> is_none x" |
102 "HOL.equal x None \<longleftrightarrow> is_none x" |
103 by (simp add: eq is_none_none) |
103 by (simp add: equal is_none_none) |
104 |
104 |
105 hide_const (open) is_none |
105 hide_const (open) is_none |
106 |
106 |
107 code_type option |
107 code_type option |
108 (SML "_ option") |
108 (SML "_ option") |
114 (SML "NONE" and "SOME") |
114 (SML "NONE" and "SOME") |
115 (OCaml "None" and "Some _") |
115 (OCaml "None" and "Some _") |
116 (Haskell "Nothing" and "Just") |
116 (Haskell "Nothing" and "Just") |
117 (Scala "!None" and "Some") |
117 (Scala "!None" and "Some") |
118 |
118 |
119 code_instance option :: eq |
119 code_instance option :: equal |
120 (Haskell -) |
120 (Haskell -) |
121 |
121 |
122 code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool" |
122 code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool" |
123 (Haskell infixl 4 "==") |
123 (Haskell infixl 4 "==") |
124 |
124 |
125 code_reserved SML |
125 code_reserved SML |
126 option NONE SOME |
126 option NONE SOME |
127 |
127 |