equal
deleted
inserted
replaced
152 |
152 |
153 datatype_new 'a deadbar = DeadBar "'a \<Rightarrow> 'a" |
153 datatype_new 'a deadbar = DeadBar "'a \<Rightarrow> 'a" |
154 datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option" |
154 datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option" |
155 datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a" |
155 datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a" |
156 datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a" |
156 datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a" |
157 datatype_new 'a deadfoo = C "'a \<Rightarrow> 'a + 'a" |
157 datatype_new 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a" |
158 |
158 |
159 datatype_new 'a dead_foo = A |
159 datatype_new 'a dead_foo = A |
160 datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" |
160 datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" |
161 |
161 |
162 datatype_new d1 = D |
162 datatype_new d1 = D |