Zulip Chat Archive
Stream: general
Topic: Try it online!
Kenny Lau (Mar 31 2018 at 05:43):
Lean is now available at tio.run
Kenny Lau (Mar 31 2018 at 05:44):
It’s a website hosted by a guy named Dennis mainly for the purpose of code-golfing competitions held in codegolf.SE
Kenny Lau (Mar 31 2018 at 05:44):
of which I have been a regular for 3 years
Kenny Lau (Mar 31 2018 at 05:45):
it was added shortly after I answered a challenge in Lean for the first time
Mario Carneiro (Mar 31 2018 at 05:58):
Re your golf:
def f:_->nat|(n+2):=f(n+1)+f n|x:=x
Kenny Lau (Mar 31 2018 at 06:00):
nice... how does that _ work?
Mario Carneiro (Mar 31 2018 at 06:01):
It figures out the type from (n+2)
Kenny Lau (Mar 31 2018 at 06:01):
you seriously should joins us! :stuck_out_tongue:
Mario Carneiro (Mar 31 2018 at 06:01):
I watch a lot
Kenny Lau (Mar 31 2018 at 06:04):
i could even prove its correctness at the end of my answer :stuck_out_tongue:
Mario Carneiro (Mar 31 2018 at 06:06):
Heh, my only answer on PPCG is a program that creates optimal golfs in another language
Kenny Lau (Mar 31 2018 at 15:26):
@Kevin Buzzard
Kenny Lau (Mar 31 2018 at 15:26):
Dennis got his thing to automatically build the latest version of mathlib once it got OK'ed by travis
Chris Hughes (Mar 31 2018 at 18:52):
Impressively fast. Is there a way to change the layout?
Kenny Lau (Mar 31 2018 at 18:52):
what kind of layout?
Chris Hughes (Mar 31 2018 at 19:13):
So it's like VScode, with goals on the right.
Kenny Lau (Mar 31 2018 at 19:14):
I'm afraid that isn't possible, since every other language on the site uses the same layout
Kenny Lau (Mar 31 2018 at 19:14):
you can still see the goals if you leave them blank, it will be displayed as an error
Kenny Lau (Apr 05 2018 at 14:13):
Lean@TIO has updated to mathlib 22e671 on lean 96c932a
Kenny Lau (Apr 24 2018 at 03:16):
https://codegolf.stackexchange.com/a/163239/48934
Andrew Ashworth (Apr 24 2018 at 04:38):
I see the top answer is very awesome, ṗṬML. Dear god what am I reading
Kevin Buzzard (Apr 24 2018 at 08:58):
I quit Lean. I'm moving over to Jelly.
Kevin Buzzard (Apr 24 2018 at 08:58):
[that's what we call Jello in the UK]
Sean Leather (Apr 24 2018 at 09:45):
@Kenny Lau Why not ℕ instead of nat?
Kenny Lau (Apr 24 2018 at 09:45):
not sure how many bytes the former is
Sean Leather (Apr 24 2018 at 09:46):
Hmm, 3 bytes according to https://mothereff.in/byte-counter .
Kenny Lau (Apr 24 2018 at 09:46):
then it saves no bytes :P
Sean Leather (Apr 24 2018 at 09:46):
Indeed.
Kenny Lau (Nov 16 2018 at 21:14):
https://codegolf.stackexchange.com/a/176122/48934
Scott Morrison (Nov 16 2018 at 21:48):
Quick, a PR!
Chris Hughes (Nov 16 2018 at 22:03):
you could import data.rat and save one character
Chris Hughes (Nov 16 2018 at 22:04):
I would have commented on stackexchange but I needed 50 reputation.
Kevin Buzzard (Nov 16 2018 at 22:04):
Are you allowed to use "the standard library"?
Mario Carneiro (Nov 16 2018 at 22:07):
yes, as long as you don't update the standard library after the challenge
Mario Carneiro (Nov 16 2018 at 22:08):
you will notice the mathematica answer is a cheeky DirichletConvolve
Mario Carneiro (Nov 16 2018 at 22:09):
(so in particular scott's strategy is disallowed by the rules)
Mario Carneiro (Nov 16 2018 at 22:11):
wait, kenny's last post on this thread is a codegolf for the number of surjections, plus a proof of correctness. Why doesn't mathlib have that?
Kenny Lau (Nov 16 2018 at 22:12):
does it?
Mario Carneiro (Nov 16 2018 at 22:13):
https://codegolf.stackexchange.com/a/163239/11143
Kenny Lau (Nov 16 2018 at 22:14):
I mean, does mathlib have that?
Kevin Buzzard (Nov 16 2018 at 22:15):
We could just start working on getting all of OEIS in, right?
Mario Carneiro (Nov 16 2018 at 22:34):
it doesn't, that's my point
Mario Carneiro (Nov 16 2018 at 22:35):
I don't see any reason we shouldn't have the stirling numbers defined, especially if you have a nice thing to prove about them
Mario Carneiro (Nov 16 2018 at 22:36):
I'm not saying we should all go out and formalize OEIS, but if someone has already gone to the trouble of formalizing some of it, I'd like to get in on that
Last updated: Dec 20 2023 at 11:08 UTC