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 9mo 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 1y 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 9mo ago by CrSb0001‭  ·  edited 9mo 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 9mo ago by CrSb0001‭  ·  edited 9mo 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 9mo ago by CrSb0001‭  ·  edited 8mo ago by CrSb0001‭

Lean 4, 111 97 bytes def d(l: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'...

posted 9mo ago by CrSb0001‭  ·  edited 8mo 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 9mo ago by CrSb0001‭

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

posted 9mo ago by CrSb0001‭  ·  edited 9mo 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 9mo ago by CrSb0001‭  ·  edited 9mo 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 10mo 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 10mo ago by CrSb0001‭

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 10mo 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 10mo ago by CrSb0001‭  ·  edited 10mo 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 1y ago by CrSb0001‭  ·  last activity 10mo ago by panadestein‭

This is somewhat of a [proof-golf]-like [cops-and-robbers]. This is the cops' thread; the robbers' thread is here Sections: Cops Scoring What is a rewrite rule? An example An example of...

1 answer  ·  posted 1y ago by CrSb0001‭  ·  last activity 1y ago by CrSb0001‭