Email Gateway (Jul 17 2020 at 17:53): Email Gateway (Jul 17 2020 at 17:53):From: "C. Diekmann" <diekmann@in.tum.de>
Soooo, it's Friday evening. When and how can I start solving
rosettacode.org tasks
in Isabelle/HOL?
Email Gateway (Jul 17 2020 at 19:03):From: Manuel Eberl <eberlm@in.tum.de>
I don't think they are tasks as such (not in the "Project Euler" sense).
If you feel like doing one in Isabelle, just do it. :)
Manuel
Email Gateway (Jul 18 2020 at 17:10):From: "C. Diekmann" <diekmann@in.tum.de>
Is it just me or does rosettacode not send out email confirmation emails?
Email Gateway (Jul 18 2020 at 22:08):From: "C. Diekmann" <diekmann@in.tum.de>
Okay, finally worked.
I started https://rosettacode.org/wiki/Category:Isabelle.
Email Gateway (Jul 24 2020 at 16:22):From: "C. Diekmann" <diekmann@in.tum.de>
I don't want to brag, but, ... okay, I'm bragging right now, ..., but I
just implemented https://rosettacode.org/wiki/Brazilian_numbers#Isabelle,
proved the claimed properties stated on rosettacode about Brazilian
numbers, and found that a stated property on rosettacode is actually wrong
<https://rosettacode.org/mw/index.php?title=Brazilian_numbers&diff=prev&oldid=309605>.
Thanks quickcheck and Isabelle/HOL! Proving stuff on a regular coding
website seems to be quite adequate. Also, it's fun :-)
Email Gateway (Jul 27 2020 at 11:56):From: Tobias Nipkow <nipkow@in.tum.de>
Cool! And such a wealth of problems one could apply Isabelle to...
Tobias
smime.p7s
Email Gateway (Jul 28 2020 at 00:51):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Nice!
Cheers,
Gerwin
Last updated: Jan 04 2025 at 20:18 UTC