Post History
Lean 4, 103 100 95 83 bytes def h:=λi=>if i<16then s!"{"0123456789ABCDEF".get ⟨i⟩}"else h (i/16)++h (i%16) Try it online! I actually am not sure how this even works, lol. I had thought...
#4: Post edited
by
CrSb0001
·
2025-04-16T19:05:29Z (2 days ago)
-12 bytes
# Lean 4, <s>103</s> <s>100</s> 95 bytes<s>It ***WOULD*** be 96 bytes, except there are 4 extra bytes of data that the 2 (two) unprintable characters take up. :(</s> Nevermind, I managed to save 5 bytes from something else. :D- ```lean
def h(i:Nat):String:=if i<16then s!"{"0123456789ABCDEF".get ⟨i⟩}"else(h (i/16))++(h (i%16))- ```
[Try it online!](https://live.lean-lang.org/#codez=LTAmFMDMAIAsAoCWAuAcgQwC4EpkGVMAnRAOwHNkBeRGRAHgEYA2TWcE+AIgAYGAmAMwAWAKxMA7AA4AnAEEAQgGEAIgFEAYpwB0ZcJmiAL8kSBL8mxbMAewLFy0cABsAzuHixoSAPTNs2ANS/Xd0QAUm9sACgIGAQUDBx8IlIKalpGFjYSaEcAQk4Abx5+YTEpOSU1TR09QxMAX04HZ0DPMP9mkLDwgGJwADd0ezhoBmkhEaFxBkkhST5wkB7+wZz8gHJ0VfroEGgAdwtCAGsc7KA)- ---
- I actually am not sure how this even works, lol. I had thought of wrapping the string indice part in a `s!""` string (similar to Python's `f`-strings) to try and avoid `(...).toString`, and it's nice to see that Lean 4 actually automatically interprets a `Char` object inside a `String` as a `String` object lol.
Only 93 more bytes until I beat the Vyxal solution xD- ---
- Hexdump since this contains unprintable characters:
- ```none
00000000 64 65 66 20 68 28 69 3a 4e 61 74 29 3a 53 74 72 |def h(i:Nat):Str|00000010 69 6e 67 3a 3d 69 66 20 69 3c 31 36 74 68 65 6e |ing:=if i<16then|00000020 20 73 21 22 7b 22 30 31 32 33 34 35 36 37 38 39 | s!"{"0123456789|00000030 41 42 43 44 45 46 22 2e 67 65 74 20 e2 9f a8 69 |ABCDEF".get ...i|00000040 e2 9f a9 7d 22 65 6c 73 65 28 68 20 28 69 2f 31 |...}"else(h (i/1|00000050 36 29 29 2b 2b 28 68 20 28 69 25 31 36 29 29 |6))++(h (i%16))|- ```
- # Lean 4, <s>103</s> <s>100</s> <s>95</s> 83 bytes
- ```lean
- def h:=λi=>if i<16then s!"{"0123456789ABCDEF".get ⟨i⟩}"else h (i/16)++h (i%16)
- ```
- [Try it online!](https://live.lean-lang.org/#codez=LTAmFMDMAIAsAoCWAuAcgQwC4EpkGVMAnRAOwHNkBeRGRAHgEYA2TWcE+AIgAYGAmAMwAWAKxMA7AA4AnAEEAQgGEAIgFEAYpwB0ZcJmiAL8kSBL8mxbMAewLFy0cABsAzuHixoSAPTNs2ANS/Xd0QAUm9sACgQCBgEFAwcfCJSCmpaRhY2EmhHAEJOAG8efmExKTklNU0dPUMTAF9OB2dAzzD/FpCw8Oi4KkBu4ERKAD4aaHpmVnZsvMLeQVEJGQUVDW1dfSNjBqbwOCCvJj9fNyRQw/CAYnAAN3R7PYZpIUehcQZJIUk+SOAr2/vcgUAOToIENaAgaAAdwshAA1rkckA)
- ---
- I actually am not sure how this even works, lol. I had thought of wrapping the string indice part in a `s!""` string (similar to Python's `f`-strings) to try and avoid `(...).toString`, and it's nice to see that Lean 4 actually automatically interprets a `Char` object inside a `String` as a `String` object lol.
- Only 60 more bytes until I beat the Vyxal solution.
- ---
- Hexdump since this contains unprintable characters:
- ```none
- 00000000 64 65 66 20 68 3a 3d ce bb 69 3d 3e 69 66 20 69 |def h:=..i=>if i|
- 00000010 3c 31 36 74 68 65 6e 20 73 21 22 7b 22 30 31 32 |<16then s!"{"012|
- 00000020 33 34 35 36 37 38 39 41 42 43 44 45 46 22 2e 67 |3456789ABCDEF".g|
- 00000030 65 74 20 e2 9f a8 69 e2 9f a9 7d 22 65 6c 73 65 |et ...i...}"else|
- 00000040 20 68 20 28 69 2f 31 36 29 2b 2b 68 20 28 69 25 | h (i/16)++h (i%|
- 00000050 31 36 29 |16)|
- ```
#3: Post edited
by
CrSb0001
·
2025-04-11T23:16:00Z (7 days ago)
-5 bytes
# Lean 4, <s>103</s> 100 bytesIt ***WOULD*** be 96 bytes, except there are 4 extra bytes of data that the 2 (two) unprintable characters take up. :(- ```lean
def h(i:Nat):String:=if i<16then("0123456789ABCDEF".get ⟨i⟩).toString else(h (i/16))++(h (i%16))- ```
- ---
- Hexdump since this contains unprintable characters:
- ```none
- 00000000 64 65 66 20 68 28 69 3a 4e 61 74 29 3a 53 74 72 |def h(i:Nat):Str|
- 00000010 69 6e 67 3a 3d 69 66 20 69 3c 31 36 74 68 65 6e |ing:=if i<16then|
00000020 28 22 30 31 32 33 34 35 36 37 38 39 41 42 43 44 |("0123456789ABCD|00000030 45 46 22 2e 67 65 74 20 e2 9f a8 69 e2 9f a9 29 |EF".get ...i...)|00000040 2e 74 6f 53 74 72 69 6e 67 20 65 6c 73 65 28 68 |.toString else(h|00000050 20 28 69 2f 31 36 29 29 2b 2b 28 68 20 28 69 25 | (i/16))++(h (i%|00000060 31 36 29 29 |16))|- ```
- # Lean 4, <s>103</s> <s>100</s> 95 bytes
- <s>It ***WOULD*** be 96 bytes, except there are 4 extra bytes of data that the 2 (two) unprintable characters take up. :(</s> Nevermind, I managed to save 5 bytes from something else. :D
- ```lean
- def h(i:Nat):String:=if i<16then s!"{"0123456789ABCDEF".get ⟨i⟩}"else(h (i/16))++(h (i%16))
- ```
- [Try it online!](https://live.lean-lang.org/#codez=LTAmFMDMAIAsAoCWAuAcgQwC4EpkGVMAnRAOwHNkBeRGRAHgEYA2TWcE+AIgAYGAmAMwAWAKxMA7AA4AnAEEAQgGEAIgFEAYpwB0ZcJmiAL8kSBL8mxbMAewLFy0cABsAzuHixoSAPTNs2ANS/Xd0QAUm9sACgIGAQUDBx8IlIKalpGFjYSaEcAQk4Abx5+YTEpOSU1TR09QxMAX04HZ0DPMP9mkLDwgGJwADd0ezhoBmkhEaFxBkkhST5wkB7+wZz8gHJ0VfroEGgAdwtCAGsc7KA)
- ---
- I actually am not sure how this even works, lol. I had thought of wrapping the string indice part in a `s!""` string (similar to Python's `f`-strings) to try and avoid `(...).toString`, and it's nice to see that Lean 4 actually automatically interprets a `Char` object inside a `String` as a `String` object lol.
- Only 93 more bytes until I beat the Vyxal solution xD
- ---
- Hexdump since this contains unprintable characters:
- ```none
- 00000000 64 65 66 20 68 28 69 3a 4e 61 74 29 3a 53 74 72 |def h(i:Nat):Str|
- 00000010 69 6e 67 3a 3d 69 66 20 69 3c 31 36 74 68 65 6e |ing:=if i<16then|
- 00000020 20 73 21 22 7b 22 30 31 32 33 34 35 36 37 38 39 | s!"{"0123456789|
- 00000030 41 42 43 44 45 46 22 2e 67 65 74 20 e2 9f a8 69 |ABCDEF".get ...i|
- 00000040 e2 9f a9 7d 22 65 6c 73 65 28 68 20 28 69 2f 31 |...}"else(h (i/1|
- 00000050 36 29 29 2b 2b 28 68 20 28 69 25 31 36 29 29 |6))++(h (i%16))|
- ```
#2: Post edited
by
CrSb0001
·
2025-04-11T10:03:00Z (8 days ago)
-3 bytes
# Lean 4, 103 bytes- ```lean
def h(i:Nat):String:=if i<16 then ("0123456789ABCDEF".get ⟨i⟩).toString else (h (i/16))++(h (i%16))- ```
- ---
- Hexdump since this contains unprintable characters:
- ```none
- 00000000 64 65 66 20 68 28 69 3a 4e 61 74 29 3a 53 74 72 |def h(i:Nat):Str|
00000010 69 6e 67 3a 3d 69 66 20 69 3c 31 36 20 74 68 65 |ing:=if i<16 the|00000020 6e 20 28 22 30 31 32 33 34 35 36 37 38 39 41 42 |n ("0123456789AB|00000030 43 44 45 46 22 2e 67 65 74 20 e2 9f a8 69 e2 9f |CDEF".get ...i..|00000040 a9 29 2e 74 6f 53 74 72 69 6e 67 20 65 6c 73 65 |.).toString else|00000050 20 28 68 20 28 69 2f 31 36 29 29 2b 2b 28 68 20 | (h (i/16))++(h |00000060 28 69 25 31 36 29 29 |(i%16))|- ```
- # Lean 4, <s>103</s> 100 bytes
- It ***WOULD*** be 96 bytes, except there are 4 extra bytes of data that the 2 (two) unprintable characters take up. :(
- ```lean
- def h(i:Nat):String:=if i<16then("0123456789ABCDEF".get ⟨i⟩).toString else(h (i/16))++(h (i%16))
- ```
- ---
- Hexdump since this contains unprintable characters:
- ```none
- 00000000 64 65 66 20 68 28 69 3a 4e 61 74 29 3a 53 74 72 |def h(i:Nat):Str|
- 00000010 69 6e 67 3a 3d 69 66 20 69 3c 31 36 74 68 65 6e |ing:=if i<16then|
- 00000020 28 22 30 31 32 33 34 35 36 37 38 39 41 42 43 44 |("0123456789ABCD|
- 00000030 45 46 22 2e 67 65 74 20 e2 9f a8 69 e2 9f a9 29 |EF".get ...i...)|
- 00000040 2e 74 6f 53 74 72 69 6e 67 20 65 6c 73 65 28 68 |.toString else(h|
- 00000050 20 28 69 2f 31 36 29 29 2b 2b 28 68 20 28 69 25 | (i/16))++(h (i%|
- 00000060 31 36 29 29 |16))|
- ```
#1: Initial revision
by
CrSb0001
·
2025-04-11T01:22:38Z (8 days ago)
# Lean 4, 103 bytes
```lean
def h(i:Nat):String:=if i<16 then ("0123456789ABCDEF".get ⟨i⟩).toString else (h (i/16))++(h (i%16))
```
---
Hexdump since this contains unprintable characters:
```none
00000000 64 65 66 20 68 28 69 3a 4e 61 74 29 3a 53 74 72 |def h(i:Nat):Str|
00000010 69 6e 67 3a 3d 69 66 20 69 3c 31 36 20 74 68 65 |ing:=if i<16 the|
00000020 6e 20 28 22 30 31 32 33 34 35 36 37 38 39 41 42 |n ("0123456789AB|
00000030 43 44 45 46 22 2e 67 65 74 20 e2 9f a8 69 e2 9f |CDEF".get ...i..|
00000040 a9 29 2e 74 6f 53 74 72 69 6e 67 20 65 6c 73 65 |.).toString else|
00000050 20 28 68 20 28 69 2f 31 36 29 29 2b 2b 28 68 20 | (h (i/16))++(h |
00000060 28 69 25 31 36 29 29 |(i%16))|
```