2025 "99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, |
2025 "99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, |
2026 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, |
2026 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, |
2027 100016, 100017, 100018, 100019, 100020"} |
2027 100016, 100017, 100018, 100019, 100020"} |
2028 |
2028 |
2029 where @{ML upto} generates a list of integers. You can print out this |
2029 where @{ML upto} generates a list of integers. You can print out this |
2030 list as an ``set'', that means enclosed inside @{text [quotes] "{"} and |
2030 list as a ``set'', that means enclosed inside @{text [quotes] "{"} and |
2031 @{text [quotes] "}"}, and separated by commas using the function |
2031 @{text [quotes] "}"}, and separated by commas using the function |
2032 @{ML [index] enum in Pretty}. For example |
2032 @{ML [index] enum in Pretty}. For example |
2033 *} |
2033 *} |
2034 |
2034 |
2035 text {* |
2035 text {* |