Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Positional Notation for Natura...

Email Gateway (Apr 14 2023 at 13:36):

From: Lawrence Paulson <lp15@cam.ac.uk>
We have a new entry, "Positional Notation for Natural Numbers in an Arbitrary Base”, by a new contributor, Charles Staats.

We demonstrate the existence and uniqueness of the base-n representation of a natural number, where n is any natural number greater than 1. This comes up when trying to translate mathematical contest problems and solutions into Isabelle/HOL.,

It’s on-line here: https://www.isa-afp.org/entries/DigitsInBase.html

Larry

Last updated: Jan 04 2025 at 20:18 UTC