Posts by 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...
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...
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 ...
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...
Python 3, 86 85 bytes The reasoning behind why this works is basically that 1. we can directly compare the ordinal values of characters (apparently) and 2. we only need that if a character is alph...
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...
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...
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 ...
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...
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...
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...
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...
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...
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...
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.)
Challenge Write a program that takes in a number greater than or equal to 0 and outputs its representation in hexadecimal (base 16). Examples 0 => 0 1 => 1 10 => A 15 ...
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...
Score: 114 ========== =Alphabet= ========== ACDEIOST+ =============== =Source string= =============== ACDEIOST+ =============== =Target string= =============== SE+CODIDACT ======...
This is somewhat of a [proof-golf]-like [cops-and-robbers]. This is the robbers' thread; the cops' thread can be found here. Sections: Robbers Determining a winner Robbers The cops wil...
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...
