Post History
Lean 4, 183 181 bytes def c(t:String)(s:Nat):String:=t.map (λc=>if Char.isAlpha c then let b:=if Char.isLower c then 'a'else 'A';let h:=(Char.toNat c-Char.toNat b+s)%26+Char.toNat b;Char.ofNat ...
#2: Post edited
by
CrSb0001
·
2025-04-17T16:19:22Z (2 days ago)
-2 bytes
# [Lean 4], 183 bytes- ```
def c(t:String)(s:Nat):String:=t.map (fun c=>if Char.isAlpha c then let b:=if Char.isLower c then 'a'else 'A';let h:=(Char.toNat c-Char.toNat b+s)%26+Char.toNat b;Char.ofNat h else c)- ```
[Try it online!](https://live.lean-lang.org/#codez=CYUwZgBAxgFALgLgMpwE4EsB2BzAlDAZwQDkBDOXZNLbBAXjgDoBbUgBwhjAFdNo6AfOkgBhABalUjdAQCCAGzYToEOGJB95IOBABG9YRHGTpBADIB7AO4hUKtRogByUk5DyCIZ7KcBuLTpi9DDGUnAWZDpQALShjOGRegDUBLgApABMAGxJcQnker5xFmCJYhDuntC4AFB1AMQgAG6k8ioARAAS7vIWEFYWqPLAAITtEAAsQA)- Honestly it's surprising that 1) you can just throw everything on one line, no matter the function's complexity, and 2) you can define anonymous functions inside of a function, which is something I did not know.
I admittedly don't have a whole lot of recent experience with Lean, so maybe there's something I'm missing that I could use to decrease bytecount.- [Lean 4]:https://lean-lang.org/
- # [Lean 4], <s>183</s> 181 bytes
- ```
- def c(t:String)(s:Nat):String:=t.map (λc=>if Char.isAlpha c then let b:=if Char.isLower c then 'a'else 'A';let h:=(Char.toNat c-Char.toNat b+s)%26+Char.toNat b;Char.ofNat h else c)
- ```
- [Try it online!](https://live.lean-lang.org/#codez=LTAmFMDMAIA8AoAuAuAyogTgSwHYHMBKeAZ2QDkBDRAtTXPZAXkQDoBbCgB2nkgFcc0AMaMAfFhgBhABYUMLLMQCCAG06zh0RNPCCV4RNABGTCdBlyFxADIB7AO7gMm7bugByCu/Ari4D0ruANz6htJM8BbyiLaUhkLAUSwxccYA1MQEAKQATABsaUkpVMZBSbaQqdLQPn7CBABQDRAwQki02PhEpHE06J0MzOxcPIDdwCLiUrLyiqrqFC46egbGplOWinaOzkJaSx5etf7ugSEr4YyR08mxJQlFt4ZGGdn5hdfFT2XXFVU1vv4hI0GgBicAANwoKk0ACIABI+FS2AA00AA6rYMCpQABCGHQAAsQA)
- Honestly it's surprising that 1) you can just throw everything on one line, no matter the function's complexity, and 2) you can define anonymous functions inside of a function, which is something I did not know.
- ---
- Hexdump since the source code contains unprintable characters:
- ```none
- 00000000 64 65 66 20 63 28 74 3a 53 74 72 69 6e 67 29 28 |def c(t:String)(|
- 00000010 73 3a 4e 61 74 29 3a 53 74 72 69 6e 67 3a 3d 74 |s:Nat):String:=t|
- 00000020 2e 6d 61 70 20 28 ce bb 63 3d 3e 69 66 20 43 68 |.map (..c=>if Ch|
- 00000030 61 72 2e 69 73 41 6c 70 68 61 20 63 20 74 68 65 |ar.isAlpha c the|
- 00000040 6e 20 6c 65 74 20 62 3a 3d 69 66 20 43 68 61 72 |n let b:=if Char|
- 00000050 2e 69 73 4c 6f 77 65 72 20 63 20 74 68 65 6e 20 |.isLower c then |
- 00000060 27 61 27 65 6c 73 65 20 27 41 27 3b 6c 65 74 20 |'a'else 'A';let |
- 00000070 68 3a 3d 28 43 68 61 72 2e 74 6f 4e 61 74 20 63 |h:=(Char.toNat c|
- 00000080 2d 43 68 61 72 2e 74 6f 4e 61 74 20 62 2b 73 29 |-Char.toNat b+s)|
- 00000090 25 32 36 2b 43 68 61 72 2e 74 6f 4e 61 74 20 62 |%26+Char.toNat b|
- 000000a0 3b 43 68 61 72 2e 6f 66 4e 61 74 20 68 20 65 6c |;Char.ofNat h el|
- 000000b0 73 65 20 63 29 |se c)|
- ```
- [Lean 4]:https://lean-lang.org/
#1: Initial revision
by
CrSb0001
·
2025-04-12T01:28:48Z (7 days ago)
# [Lean 4], 183 bytes ``` def c(t:String)(s:Nat):String:=t.map (fun c=>if Char.isAlpha c then let b:=if Char.isLower c then 'a'else 'A';let h:=(Char.toNat c-Char.toNat b+s)%26+Char.toNat b;Char.ofNat h else c) ``` [Try it online!](https://live.lean-lang.org/#codez=CYUwZgBAxgFALgLgMpwE4EsB2BzAlDAZwQDkBDOXZNLbBAXjgDoBbUgBwhjAFdNo6AfOkgBhABalUjdAQCCAGzYToEOGJB95IOBABG9YRHGTpBADIB7AO4hUKtRogByUk5DyCIZ7KcBuLTpi9DDGUnAWZDpQALShjOGRegDUBLgApABMAGxJcQnker5xFmCJYhDuntC4AFB1AMQgAG6k8ioARAAS7vIWEFYWqPLAAITtEAAsQA) Honestly it's surprising that 1) you can just throw everything on one line, no matter the function's complexity, and 2) you can define anonymous functions inside of a function, which is something I did not know. I admittedly don't have a whole lot of recent experience with Lean, so maybe there's something I'm missing that I could use to decrease bytecount. [Lean 4]:https://lean-lang.org/