Email Gateway (Mar 03 2022 at 14:45): Email Gateway (Mar 03 2022 at 14:45):From: Lawrence Paulson <lp15@cam.ac.uk>
This is a follow-up to a message I sent about a month ago.
We have a couple of real gems hidden among our various examples directories. One of them is an old example of mine, a port of a proof in type theory that Ackermann’s function is not primitive recursive. Another is the construction of the real numbers using Dedekind cuts, which is on the one hand redundant (for some reason another construction of the reals was substituted) but on the other hand iconic (thanks to AUTOMATH).
I think that both of them should be moved to the AFP, and we should look for others. Any other opinions?
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC