Post History

60%

+1 −0

Lean 4, 111 bytes def c(l:List Nat):List Nat:=((λx=>((l.reverse).drop x).count (l.reverse)[x]!)<$>(List.range l.length)).reverse Try it online! Given how verbose Lean syntax is, and h...

posted 5d ago by CrSb0001‭ · edited 5d ago by CrSb0001‭

Answer

#3: Post edited by

CrSb0001‭ · 2025-04-14T19:28:33Z (5 days ago)

Copy Link

Raw

Markdown

#2: Post edited by

CrSb0001‭ · 2025-04-14T19:28:24Z (5 days ago)

Copy Link

Raw

Markdown

# [Lean 4], 111 bytes
```lean
def c(l:List Nat):List Nat:=((λx=>((l.reverse).drop x).count (l.reverse)[x]!)<$>(List.range l.length)).reverse
```
[Try it online!]
Given how verbose Lean syntax is, and how you can't really assign variables to keywords in a way that it saves bytes the vast majority of the time, if at all, I doubt there's a way to save any more bytes from here. I think 111 might actually be the limit.
And the only reason that I have to reverse the list is because while Lean does have a function to drop elements, it only does so from the left, which we really don't want here.
---
Hexdump since this contains unprintable characters:
```none
00000000 64 65 66 20 64 28 6c 3a 4c 69 73 74 20 4e 61 74 |def d(l:List Nat|
00000010 29 3a 4c 69 73 74 20 4e 61 74 3a 3d 28 28 ce bb |):List Nat:=((..|
00000020 78 3d 3e 28 28 6c 2e 72 65 76 65 72 73 65 29 2e |x=>((l.reverse).|
00000030 64 72 6f 70 20 78 29 2e 63 6f 75 6e 74 20 28 6c |drop x).count (l|
00000040 2e 72 65 76 65 72 73 65 29 5b 78 5d 21 29 3c 24 |.reverse)[x]!)<$|
00000050 3e 28 4c 69 73 74 2e 72 61 6e 67 65 20 6c 2e 6c |>(List.range l.l|
00000060 65 6e 67 74 68 29 29 2e 72 65 76 65 72 73 65 |ength)).reverse|
```
~~[Lean 4]:https://lean-lang.org/~~

# [Lean 4], 111 bytes
```lean
def c(l:List Nat):List Nat:=((λx=>((l.reverse).drop x).count (l.reverse)[x]!)<$>(List.range l.length)).reverse
```
[Try it online!]
Given how verbose Lean syntax is, and how you can't really assign variables to keywords in a way that it saves bytes the vast majority of the time, if at all, I doubt there's a way to save any more bytes from here. I think 111 might actually be the limit.
And the only reason that I have to reverse the list is because while Lean does have a function to drop elements, it only does so from the left, which we really don't want here.
---
Hexdump since this contains unprintable characters:
```none
00000000 64 65 66 20 64 28 6c 3a 4c 69 73 74 20 4e 61 74 |def d(l:List Nat|
00000010 29 3a 4c 69 73 74 20 4e 61 74 3a 3d 28 28 ce bb |):List Nat:=((..|
00000020 78 3d 3e 28 28 6c 2e 72 65 76 65 72 73 65 29 2e |x=>((l.reverse).|
00000030 64 72 6f 70 20 78 29 2e 63 6f 75 6e 74 20 28 6c |drop x).count (l|
00000040 2e 72 65 76 65 72 73 65 29 5b 78 5d 21 29 3c 24 |.reverse)[x]!)<$|
00000050 3e 28 4c 69 73 74 2e 72 61 6e 67 65 20 6c 2e 6c |>(List.range l.l|
00000060 65 6e 67 74 68 29 29 2e 72 65 76 65 72 73 65 |ength)).reverse|
```
[Lean 4]:https://lean-lang.org/
[Try it online!]:https://live.lean-lang.org/#codez=LTAEEYCYBZQIwJ4BcCmBnAUAExQM3gBQA2AXADICWaSoAcgIZICU5VNDSJAvAJJYB0AJwCuAO1BYA9qCIoanLkSEoAbikFoUAbkFzhg0QQKBu4AAeXAHwEk/LIMkAHUKab8AxpLHyA2qYC6AIRMADwAJFaU1EL0ogDmKDL8snFIABZMrrpqGigYGCAQ4ODwyOjYeKBuxKzUdIwskeyM3EZmlkZKWeqarnaOzq4eXqDEytk9voEh4QSN0XEJSsmxaRlj3bkYAMSq9EQB8KDe4AA0p5AnFxenNycAzPd+27v7h94PAOwnAKwn0CcATku92BADYTqCnjsVHsDnAjqcAVCXnCEZcns8Ya83GjzsDrmdCQ87sisQcce8Tl9fv8gRcHhdwZDMbDKmikSzsWjIH4gA

#1: Initial revision by

CrSb0001‭ · 2025-04-14T19:27:05Z (5 days ago)

Copy Link

Raw

Markdown

# [Lean 4], 111 bytes

```lean
def c(l:List Nat):List Nat:=((λx=>((l.reverse).drop x).count (l.reverse)[x]!)<$>(List.range l.length)).reverse
```
[Try it online!]

Given how verbose Lean syntax is, and how you can't really assign variables to keywords in a way that it saves bytes the vast majority of the time, if at all, I doubt there's a way to save any more bytes from here. I think 111 might actually be the limit.

And the only reason that I have to reverse the list is because while Lean does have a function to drop elements, it only does so from the left, which we really don't want here.

---

Hexdump since this contains unprintable characters:
```none
00000000 64 65 66 20 64 28 6c 3a 4c 69 73 74 20 4e 61 74  |def d(l:List Nat|
00000010 29 3a 4c 69 73 74 20 4e 61 74 3a 3d 28 28 ce bb  |):List Nat:=((..|
00000020 78 3d 3e 28 28 6c 2e 72 65 76 65 72 73 65 29 2e  |x=>((l.reverse).|
00000030 64 72 6f 70 20 78 29 2e 63 6f 75 6e 74 20 28 6c  |drop x).count (l|
00000040 2e 72 65 76 65 72 73 65 29 5b 78 5d 21 29 3c 24  |.reverse)[x]!)<$|
00000050 3e 28 4c 69 73 74 2e 72 61 6e 67 65 20 6c 2e 6c  |>(List.range l.l|
00000060 65 6e 67 74 68 29 29 2e 72 65 76 65 72 73 65     |ength)).reverse|
```

[Lean 4]:https://lean-lang.org/

Communities

Post History