Post History
Lean4, 113 56 bytes #eval(λx=>x^32767%4^8)<$>(λx=>1+x*2)<$>(List.range 49) Try it online! Something to notice is that you apparently don't need type signatures in functions...
#2: Post edited
by
CrSb0001
·
2025-05-30T15:40:13Z (1 day ago)
-59 bytes
# Lean4, 113 bytes- ```lean
def m(i)(j:=4^8):=Id.run dolet mut c:=1while c%i>0do c:=c+jreturn c/i#eval m<$>(λx=>1+x*2)<$>(List.range 49)- ```
- [Try it online!]
- ---
Something to notice is that you apparently don't need type signatures in functions, and that mapping is right associative.- ---
- Obligatory hexdump since this contains unprintable characters:
- ```none
00000000 64 65 66 20 6d 28 69 29 28 6a 3a 3d 34 5e 38 29 |def m(i)(j:=4^8)|00000010 3a 3d 49 64 2e 72 75 6e 20 64 6f 0a 6c 65 74 20 |:=Id.run do.let |00000020 6d 75 74 20 63 3a 3d 31 0a 77 68 69 6c 65 20 63 |mut c:=1.while c|00000030 25 69 3e 30 64 6f 20 63 3a 3d 63 2b 6a 0a 72 65 |%i>0do c:=c+j.re|00000040 74 75 72 6e 20 63 2f 69 0a 23 65 76 61 6c 20 6d |turn c/i.#eval m|00000050 3c 24 3e 28 ce bb 78 3d 3e 31 2b 78 2a 32 29 3c |<$>(..x=>1+x*2)<|00000060 24 3e 28 4c 69 73 74 2e 72 61 6e 67 65 20 34 39 |$>(List.range 49|00000070 29 |)|- ```
[Try it online!]:https://live.lean-lang.org/#codez=CYUwZgBAtgFAlgShgKwFwF4AsA9AHAjASWADoAnAVwDsJgB7AKABsQAXaC9gYwwEYGA7gAs4LCFwCkcAHwAGeuIxcA1MgZk2FMjS4B6OAwDEIAG4BDJtAA8AEmkxA3cAAPdNN7KnAKgBMCW/YAZOABnVnIzKgBzEAhMAE4EIA
- # Lean4, <s>113</s> 56 bytes
- ```lean
- #eval(λx=>x^32767%4^8)<$>(λx=>1+x*2)<$>(List.range 49)
- ```
- [Try it online!]
- ---
- <s>Something to notice is that you apparently don't need type signatures in functions</s> or a function at all, in that case, and that mapping is right associative.
- ---
- Obligatory hexdump since this contains unprintable characters:
- ```none
- 00000000 23 65 76 61 6c 28 ce bb 78 3d 3e 78 5e 33 32 37 |#eval(..x=>x^327|
- 00000010 36 37 25 34 5e 38 29 3c 24 3e 28 ce bb 78 3d 3e |67%4^8)<$>(..x=>|
- 00000020 31 2b 78 2a 32 29 3c 24 3e 28 4c 69 73 74 2e 72 |1+x*2)<$>(List.r|
- 00000030 61 6e 67 65 20 34 39 29 |ange 49)|
- ```
- [Try it online!]:https://live.lean-lang.org/#codez=MQUwbghgNgFI3cAA8C8A+BA9AzAJgOwDZcBSAFnQA4BKAHgBIV5kUBGAagQCpsb6YAZAJYBnAC4A6AE4QAdgHMQAAhIBOSkA
#1: Initial revision
by
CrSb0001
·
2025-05-29T19:57:06Z (2 days ago)
# Lean4, 113 bytes ```lean def m(i)(j:=4^8):=Id.run do let mut c:=1 while c%i>0do c:=c+j return c/i #eval m<$>(λx=>1+x*2)<$>(List.range 49) ``` [Try it online!] --- Something to notice is that you apparently don't need type signatures in functions, and that mapping is right associative. --- Obligatory hexdump since this contains unprintable characters: ```none 00000000 64 65 66 20 6d 28 69 29 28 6a 3a 3d 34 5e 38 29 |def m(i)(j:=4^8)| 00000010 3a 3d 49 64 2e 72 75 6e 20 64 6f 0a 6c 65 74 20 |:=Id.run do.let | 00000020 6d 75 74 20 63 3a 3d 31 0a 77 68 69 6c 65 20 63 |mut c:=1.while c| 00000030 25 69 3e 30 64 6f 20 63 3a 3d 63 2b 6a 0a 72 65 |%i>0do c:=c+j.re| 00000040 74 75 72 6e 20 63 2f 69 0a 23 65 76 61 6c 20 6d |turn c/i.#eval m| 00000050 3c 24 3e 28 ce bb 78 3d 3e 31 2b 78 2a 32 29 3c |<$>(..x=>1+x*2)<| 00000060 24 3e 28 4c 69 73 74 2e 72 61 6e 67 65 20 34 39 |$>(List.range 49| 00000070 29 |)| ``` [Try it online!]:https://live.lean-lang.org/#codez=CYUwZgBAtgFAlgShgKwFwF4AsA9AHAjASWADoAnAVwDsJgB7AKABsQAXaC9gYwwEYGA7gAs4LCFwCkcAHwAGeuIxcA1MgZk2FMjS4B6OAwDEIAG4BDJtAA8AEmkxA3cAAPdNN7KnAKgBMCW/YAZOABnVnIzKgBzEAhMAE4EIA