Module defined_real 

Which functions may define a real number: the real number whose digits in base 3 are f, the real number approximated by f.

A defined real reads its function only as a refinement needs it, and every tier reads it in a context of its own, at whatever moment a comparison, a floor or a printed digit asks. That is sound only for a function whose answer depends on its argument alone and whose call does nothing but answer. The phrase is the builtin definedReal(kind, base, name, (n: Int) -> name(n)), and every tier reads its four arguments as the phrase writes them, so a program is refused, before it runs, when it calls definedReal in any other form, and when a function it defines a real by:

• is not one the program defines;
• does not take exactly one Int;
• declares an answer other than an Int (digits) or an Int or a Rational (approximations);
• does more than answer — shows, reads or writes a file, sends, launches, chooses — or calls a function that does (crate::optimize::effects);
• or reads a variable of the program, itself or through a function it calls.

Functions

check

The first function the program defines a real number by that cannot define one, refused in words naming it; Ok when there is none.