Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Rosetta Code


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip Email Gateway (Jul 28 2020 at 00:51):

From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Nice!

Cheers,
Gerwin


Last updated: Jul 15 2022 at 23:21 UTC