equal
deleted
inserted
replaced
1169 |
1169 |
1170 instance .. |
1170 instance .. |
1171 |
1171 |
1172 end |
1172 end |
1173 |
1173 |
|
1174 instantiation rat :: partial_term_of |
|
1175 begin |
|
1176 |
|
1177 instance .. |
|
1178 |
|
1179 end |
|
1180 |
|
1181 lemma [code]: |
|
1182 "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Var p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])" |
|
1183 "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Ctr 0 [l, k]) == |
|
1184 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Fract'') |
|
1185 (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], |
|
1186 Typerep.Typerep (STR ''Rat.rat'') []]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k)" |
|
1187 by (rule partial_term_of_anything)+ |
|
1188 |
1174 instantiation rat :: narrowing |
1189 instantiation rat :: narrowing |
1175 begin |
1190 begin |
1176 |
1191 |
1177 definition |
1192 definition |
1178 "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Fract) narrowing) narrowing" |
1193 "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Fract) narrowing) narrowing" |