CrSb0001‭

Lean is an interactive theorem prover and a functional programming language created in 2013. What tips do you have for golfing in Lean? Tips should be specific to Lean ("remove comments" is not an...

0 answers  ·  posted 6d ago by CrSb0001‭

Also posted here on CodeGolf.SE Brief introduction to Emmental: Emmental is a self-modifying programming language defined by a meta-circular interpreter. It is a stack based language, but also ...

0 answers  ·  posted 12mo ago by CrSb0001‭

Lean 4, 115 109 104 89 bytes Note: had to update bytecount to take into account non-printable characters. For anyone who isn't familiar with Lean, it's basically an interactive theorem prover t...

posted 7d ago by CrSb0001‭  ·  edited 2d ago by CrSb0001‭

Inspiration: Leetcode's [3Sum] linkLink on CG&CC Problem Given an array nums of n (not necessarily distinct) integers, and given a target number target, return an array of all of the unique...

2 answers  ·  posted 4mo ago by CrSb0001‭  ·  last activity 29d ago by panadestein‭

Python 3.8, 44 bytes Uses a modulus of 2**16 == 4**8 == 65536. for i in range(1,98,2):print(pow(i,-1,4**8)) How it works: for i in # Iterator ra...

posted 14d ago by CrSb0001‭

Assignment expressions (Python 3.8+) The assignment expression (aka the walrus operator) := was introduced in Python 3.8 as a result of PEP 572, which can be used inline to assign a variable as pa...

posted 14d ago by CrSb0001‭

Emmental, 51 bytes #72.#101.#108::..#111:.#44.#32.#87..#114..#100.#33. Try it online! Basically what goes on is #[num] pushes the ASCII value of num onto the top of the stack, : duplicates t...

posted 12d ago by CrSb0001‭

Python 3, 26 bytes lambda n:(n+(n*n+4)**.5)/2 We can actually just compute this directly, although I could have taken an alternate path considering the fact that, given $R_n$ as the ratio betwe...

posted 9d ago by CrSb0001‭  ·  edited 8h ago by CrSb0001‭

Python 3, 131 75 62 bytes f=lambda n:n>0and 2+3*f(n-1)+4*f(n-2)+2*sum(map(f,range(n-2))) I know, a one-liner is boring. This is because I apparently didn't need a separate function/lambda to...

posted 9d ago by CrSb0001‭  ·  edited 7d ago by CrSb0001‭

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...

posted 6d ago by CrSb0001‭  ·  edited 8h ago by CrSb0001‭

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...

posted 5d ago by CrSb0001‭

Python 3, 50 bytes We can simply omit the lambda name since we don't refer to it anywhere in the lambda definition. lambda l:[l[:i+1].count(j)for i,j in enumerate(l)] Example usage in the term...

posted 2d ago by CrSb0001‭

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 2d ago by CrSb0001‭  ·  edited 2d ago by CrSb0001‭

Python 3.8, 57 bytes -2 bytes (2025-04-02) def m(c): for _ in range(16):(z:=c)*z+c return abs(z)<2 Try it online (59 byte version) Returns False if c (a complex number) is not part o...

posted 16d ago by CrSb0001‭  ·  edited 15d ago by CrSb0001‭

Lean 4, 39 bytes def x(i:String):String:=s!"Hello, {i}!" Try it online! (Note that TIO only supports Lean 3, so I sadly am unable to use a link from there.)

posted 6d ago by CrSb0001‭