1171 "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int") |
1171 "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int") |
1172 attach {* |
1172 attach {* |
1173 fun rat_of_int i = (i, 1); |
1173 fun rat_of_int i = (i, 1); |
1174 *} |
1174 *} |
1175 |
1175 |
1176 setup {* |
1176 declaration {* |
1177 Nitpick_HOL.register_frac_type_global @{type_name rat} |
1177 Nitpick_HOL.register_frac_type @{type_name rat} |
1178 [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), |
1178 [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), |
1179 (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}), |
1179 (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}), |
1180 (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}), |
1180 (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}), |
1181 (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}), |
1181 (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}), |
1182 (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}), |
1182 (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}), |