pub enum Builtin {
Show 26 variants
Infinitesimal,
StandardPart,
IsInfinitesimal,
IsLimited,
InfinitelyClose,
GeneratorOf,
LimitOf,
Provisional,
AtTheLimit,
TripCount,
AffinePower,
PolynomialFlow,
CycleAt,
SearchCandidates,
StateSize,
EveryNatural,
ExactSqrt,
ExactExp,
ExactLn,
ExactPi,
ExactE,
ExactOmega,
HybridFlow,
FirstExit,
ExactPower,
OrderedInfinitesimal,
}Expand description
A builtin of the exact extension.
Variants§
Infinitesimal
infinitesimal(name, modulus, allowed…): a fresh infinitesimal whose reciprocal’s residue
modulo modulus is one of allowed.
StandardPart
standardPart(x[, at]), isInfinitesimal(x[, at]), isLimited(x[, at]),
infinitelyClose(x, y[, at]): the standard part and the predicates, relative to the infinitesimal
at when it is given.
IsInfinitesimal
IsLimited
InfinitelyClose
GeneratorOf
The infinite integer 1/dt an infinitesimal generates.
LimitOf
A value read under a named limit rule.
Provisional
A search’s answer with its evidence: the steps it took and the revisions it made.
AtTheLimit
The statement At the limit, take …: names a rule, answers nothing.
TripCount
AffinePower
PolynomialFlow
CycleAt
SearchCandidates
StateSize
EveryNatural
A search over every natural that reached a run unresolved.
ExactSqrt
The exact square root, exponential and natural logarithm, which sqrt, exp and ln are in
a context that declares an exact type.
ExactExp
ExactLn
ExactPi
π and e exactly, which pi and e are in a context that declares an exact type.
ExactE
ExactOmega
ω, the first infinite ordinal, which omega is in an Ordinal context.
HybridFlow
The end state of a loop whose state flows between jumps.
FirstExit
How many passes a loop makes whose guard compares terms linear in a counter it steps.
ExactPower
base ** exponent to an exponent that is an exact number, which ** and pow are when their
exponent is one: a fraction p/q takes the real q-th root to the p-th power.
OrderedInfinitesimal
orderedInfinitesimal(name, larger, smaller, modulus, allowed…): a fresh infinitesimal much
smaller than the infinitesimal larger and much larger than smaller, either bound nothing
when the declaration does not name it.