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 2mo 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, 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 2mo ago by CrSb0001‭  ·  edited 2mo 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 2mo ago by CrSb0001‭  ·  edited 2mo 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 3mo 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 3mo 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 3mo 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 2mo ago by CrSb0001‭  ·  edited 14d 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 2mo ago by CrSb0001‭  ·  edited 2mo 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 2mo ago by CrSb0001‭  ·  edited 2mo 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 2mo 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 2mo ago by CrSb0001‭  ·  edited 19d ago by CrSb0001‭

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

posted 2mo ago by CrSb0001‭  ·  edited 2mo ago by CrSb0001‭

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

posted 20d ago by CrSb0001‭  ·  edited 19d ago by CrSb0001‭

Lean 4, 232 bytes def r(i):=Id.run do let M:=[999,899,499,399,99,89,49,39,9,8,4,3,0] let N:=["M","CM","D","CD","C","XC","L","XL","X","IX","V","IV","I"] let mut s:="" let mut n:=i for x in Lis...

posted 19d ago by CrSb0001‭