Int53 traps rather than wraps. JS's Number silently loses precision past 2^53, so failing makes the semantics easier to line up than quietly returning a wrong answer.

The elements of Arr.range n: the whole numbers below n, and none of them when n is not positive. Every element is smaller than n, so an argument that is an Int53 bounds them all and no element of the answer can be out of range.

Integer division is pinned to truncation. Lean's / is floor division (-7 / 2 = -4), which disagrees with JS's Math.trunc(-7 / 2) = -3.

Strings are left out even though they are ordered: JS's < orders them by UTF-16 unit, so a String min would have to route through __strcmp the way the ordering comparisons do.

The whitespace trim strips. Written out rather than delegated to Char.isWhitespace because the generated code has to strip exactly this set, and JS's own trim also takes NBSP, the BOM and the line separators.

Case conversion is ASCII only. JS's toUpperCase is neither: it maps ß to SS, which changes the length of the string.

Where needle first sits in the haystack, counted in code points. The empty needle sits at 0, so this answers some 0 on the empty haystack too.

Splitting on the empty separator gives back the whole string. JS's split("") instead returns the UTF-16 units, which is why the generated code cannot call it unguarded.

s written n times over, one copy at a time. The halving the emitted helper uses is proved equal to this in Correct; this is the shape the docstring claims.

Writing an existing key leaves it where it is and writing a new one appends, which is what Map.set does. Iteration order is observable through keys, so the two have to agree on it.

The digits read as a number, with no bound on the answer. A character that is not a digit contributes its code point less 48, which parseInt53 throws away by printing the answer back.

Reading an Int53 back from its decimal spelling. The answer has to print as the string it was read from, so what this accepts is exactly what toString prints: "007", "+5", " 5" and "-0" are refused, and so is anything outside the Int53 range.

Indices count code points, and one outside the string traps the way an array read does. Clamping is what JS's own substring would do, and silently returning a shorter string is worse than failing.

Bounds count elements and one outside the array traps, exactly as substring's do on a String.

A function-typed parameter holds the name of a declaration, so applying it is an ordinary call to that name. Anything else bound to the name is rejected by the compiler, never here.

What a pattern binds when it matches the value, and nothing when it does not. Matching needs no evaluation, so Step runs the same function in one transition rather than decomposing the scrutinee across frames.

The first arm whose pattern matches, with what it bound. Arms are tried in order, so an arm is reached only when every earlier one failed.

The order the keys of a sortByKey are compared by. Int53 and String are the only key types the compiler lets through, and both orders are the ones the subset already has: ≤ on Int53, and the code-point order compare gives, which is what < on two strings already means here.

The keys are all Int53 or all String. A well-typed program cannot reach the other case: the key type is settled by the compiler before the walk runs.

List.mergeSort is the model rather than a sort of our own so that what it already proves — the answer is a permutation of the input, and equal keys keep the order they came in — is what an author reasons with.

Every value the sort answers with came in, which is what carries a property of the elements across it. List.mergeSort gives the permutation; the pairing gives the element back.

and / or are handled first because JS's && / || short-circuit. Evaluating both sides would make false && (1 / 0) give false in JS and a trap here, splitting the differential test at once.

Stops at the first element the predicate accepts, so a predicate that would trap on a later element never sees it.

A fold over a value of a declared type, from the leaves up. Each node is rebuilt with every field that came round replaced by the fold's answer for it, and the alternatives then read the rebuilt node exactly as a match's do — so the walk is here and not in the subset.

The recursion is on the value and not on the fuel, the way evalMapItems walks its list at the fuel it was handed. That is what keeps a fold one expression node however deep the value is, and so what keeps Cost.cost readable off the syntax.

A value whose constructor the declared type does not name, and a field the declaration names that the value does not carry, are both refused rather than guessed at: a well-typed program reaches neither.

A field the declaration gives a list of the type coming round. Anything but an array is a value no well-typed program builds, so the walk refuses it rather than folding something else.

The upper bound on call depth. Differential test calls are built so as not to exceed it.

Calls one exported function. The argument types are checked against the declaration at the entry.