Sort numbers lexicographically: Difference between revisions
Content added Content deleted
(→{{header|Common Lisp}}: Implemented Common Lisp version) |
No edit summary |
||
| Line 476: | Line 476: | ||
{{out}} |
{{out}} |
||
<pre>[1,10,11,12,13,2,3,4,5,6,7,8,9]</pre> |
<pre>[1,10,11,12,13,2,3,4,5,6,7,8,9]</pre> |
||
=={{header|Isabelle}}== |
|||
{{works with|Isabelle|2020}} |
|||
<lang Isabelle>theory LexList |
|||
imports |
|||
Main |
|||
"~~/src/HOL/Library/Char_ord" |
|||
"~~/src/HOL/Library/List_Lexorder" |
|||
begin |
|||
definition ord_ascii_zero :: nat where |
|||
"ord_ascii_zero == of_char (CHR ''0'')" |
|||
text‹Get the string representation for a single digit.› |
|||
definition ascii_of_digit :: "nat ⇒ string" where |
|||
"ascii_of_digit n ≡ if n ≥ 10 then undefined else [char_of (n + ord_ascii_zero)]" |
|||
fun ascii_of :: "nat ⇒ string" where |
|||
"ascii_of n = (if n < 10 |
|||
then ascii_of_digit n |
|||
else ascii_of (n div 10) @ ascii_of_digit (n mod 10))" |
|||
lemma ‹ascii_of 123 = ''123''› by code_simp |
|||
value ‹sort (map ascii_of (upt 1 13))› |
|||
end</lang> |
|||
{{out}} |
|||
<pre>"[''1'', ''10'', ''11'', ''12'', ''2'', ''3'', ''4'', ''5'', ''6'', ''7'', ''8'', ''9'']" |
|||
:: "char list list"</pre> |
|||
=={{header|J}}== |
=={{header|J}}== |
||