111 instantiation prod :: (full_small, full_small) full_small |
111 instantiation prod :: (full_small, full_small) full_small |
112 begin |
112 begin |
113 |
113 |
114 definition |
114 definition |
115 "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y), |
115 "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y), |
116 %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d" |
116 %u. let T1 = (Typerep.typerep (TYPE('a))); |
|
117 T2 = (Typerep.typerep (TYPE('b))) |
|
118 in Code_Evaluation.App (Code_Evaluation.App ( |
|
119 Code_Evaluation.Const (STR ''Product_Type.Pair'') |
|
120 (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) |
|
121 (t1 ())) (t2 ()))) d) d" |
117 |
122 |
118 instance .. |
123 instance .. |
119 |
124 |
120 end |
125 end |
121 |
126 |
227 |
232 |
228 instantiation prod :: (check_all, check_all) check_all |
233 instantiation prod :: (check_all, check_all) check_all |
229 begin |
234 begin |
230 |
235 |
231 definition |
236 definition |
232 "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))" |
237 "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), |
|
238 %u. let T1 = (Typerep.typerep (TYPE('a))); |
|
239 T2 = (Typerep.typerep (TYPE('b))) |
|
240 in Code_Evaluation.App (Code_Evaluation.App ( |
|
241 Code_Evaluation.Const (STR ''Product_Type.Pair'') |
|
242 (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) |
|
243 (t1 ())) (t2 ()))))" |
233 |
244 |
234 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list" |
245 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list" |
235 where |
246 where |
236 "enum_term_of_prod = (%_ _. map (%(x, y). Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) x) y) (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))" |
247 "enum_term_of_prod = (%_ _. map (%(x, y). |
|
248 let T1 = (Typerep.typerep (TYPE('a))); |
|
249 T2 = (Typerep.typerep (TYPE('b))) |
|
250 in Code_Evaluation.App (Code_Evaluation.App ( |
|
251 Code_Evaluation.Const (STR ''Product_Type.Pair'') |
|
252 (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y) |
|
253 (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ()))) " |
237 |
254 |
238 instance .. |
255 instance .. |
239 |
256 |
240 end |
257 end |
241 |
258 |