How many elements, as the Int53 the subset counts in.

The whole numbers below n, and none of them where n is not positive.

This is the array a body folds over when it has to run a number of times rather than once per element it was handed. It is the one array whose length a value rather than the syntax decides, so Bound asks that the program text bound that value -- Arr.range (min (max n 0) 64) -- exactly as it does of a repeat.

The element at an index. An index outside the array traps rather than answering default; what is written here is what the total function has to say in a case the certificate never reaches.

The key types the subset orders an array by. le is the order the author reasons with, and agrees is what ties it to the order the generated code puts the elements in; scalar is what says the key is one the comparison is defined on, which is what keeps the two sides from parting company on a value neither order was written for.

The elements ordered by their key. List.mergeSort is what the generated code computes too, so what it proves is what ships: the answer is a permutation of the input, and elements whose keys compare equal keep the order they came in.

The elements from lo up to but not including hi. Bounds that do not fit trap.

The first n elements, or all of them where there are fewer.

Everything after the first n elements.

The elements added up. Leaving Int53 on the way traps, as the addition does.

How many elements p holds of.

The first element, or none where there is none. Unlike get, this never traps — the empty case is an answer rather than a read past the end.

The last element, or none where there is none.

The arrays run together, in the order they come in.

Each element replaced by an array, and those run together.

How many code points, as the Int53 the subset counts in. JS's own .length counts UTF-16 units; the generated code goes through Array.from so that it counts what this counts.

Strips space, tab, carriage return and newline. JS's trim also takes NBSP, the BOM and the line separators, so an author who wants exactly those four writes this.

ASCII case folding. String.toUpper is full Unicode and can change the length of the string.

ASCII case folding. String.toLower is full Unicode.

Splitting on the empty separator gives back the whole string, where JS's split("") would give the UTF-16 units.

The code points from lo up to but not including hi. Bounds that do not fit trap.

Reads back what Int53.toString prints, and nothing else. "007", "+5", " 5" and "-0" are refused along with everything outside the Int53 range, because none of them is what the printer would have written. JS's own Number() reads all four.

Where t first sits in s, counted in code points, or none when it does not sit there at all. The empty needle sits at 0. JS's own indexOf counts UTF-16 units and answers -1 for absence.

The strings in order with sep between them, the way JS's own Array.prototype.join puts it together. An empty list joins to the empty string.

Every occurrence of pat, not just the first: this is JS's replaceAll, where JS's replace takes only the first. An empty pat leaves s as it is, where replaceAll("", r) inserts at every position.

s written n times over, counted in code points the way Str.length counts them. A count of zero or less gives the empty string, where JS's own repeat throws on a negative one. A result longer than an Int53 traps, the same bound Str.length lives under.

s widened to n code points by writing pad in front of it, cut to fit exactly. A width s already reaches, and an empty pad, leave s as it is. JS's own padStart counts UTF-16 units, so it pads astral text short.

The width already reached is the case a padding theorem starts from, and the guard is what says so.

Truncating division, which is what the generated Math.trunc performs. Lean's / on Int rounds towards negative infinity, so -7 / 2 is -4 there and -3 here. A zero divisor traps.

The remainder that goes with div. A zero divisor traps.

Division rounding towards negative infinity, where div rounds towards zero: divFloor (-7) 2 is -4 and div (-7) 2 is -3. A zero divisor traps, as div does.

Division rounding towards positive infinity.

Division rounding a half away from zero, which is how an amount in minor units is rounded where nothing says otherwise: divRound 5 2 is 3 and divRound (-5) 2 is -3. The remainder is compared against what is left of the divisor rather than doubled, so a divisor near the top of the range decides the same way as any other rather than trapping on the way to the answer.

The decimal spelling. JS's String(n) falls back to exponent notation only at 1e21, which is above the Int53 range, so the two agree on every Int53.

The day a civil date falls on, counting from 1970-01-01, which is day zero. A month outside 1..12 or a day outside the month is not refused: the arithmetic carries it, so 2026-13-01 is 2027-01-01.

The four-hundred-year era a day falls in, counted from the one holding 0000-03-01. Written out because the three readings below each need it, and the subset has nothing to share it with.

The day's place inside its era, in 0..146096.

The day's year inside its era, in 0..399.

The day's place inside its year, counting from the first of March, in 0..365.

The month in March-first numbering, in 0..11. January and February are 10 and 11, which is what makes a leap day the last day of the year and the arithmetic above carry no special case.

The civil year the day falls in.

The civil month, 1..12.

The civil day of the month, 1..31.

The day of the week, 0 for Sunday through 6 for Saturday. Day zero is a Thursday.

Whether a year carries a leap day, by the Gregorian rule.

How many days a month holds, read as the distance to the first of the next month so that it cannot disagree with fromCivil about a leap February.

The day an instant falls in, an instant being milliseconds from the epoch. An instant before the epoch belongs to the day it is inside, which is divFloor and not div.

The first instant of a day.

What the check accepted, with why it refused dropped.

The subset's arbitrary-precision integer. Int is already the one that has to fit in a JS number, so the one that does not is a wrapper: the two are told apart by their type, never by their values.

== is the subset's equality, so it is the one on the value rather than the one DecidableEq would derive through the wrapper.

Truncating division, as on Int53. A zero divisor traps.

A Map on the JS side. The entries are a list rather than a set because iteration order is observable through keys, so the two sides have to agree on it: a write to a key already present leaves it where it is, and a write to a new one appends.

Writing a key already present leaves it where it is; writing a new one appends.

How many entries, as the Int53 the subset counts in.

What k is bound to, or dflt where it is bound to nothing.

An array indexed by a key read off each element. Where two elements give the same key the later one wins, and keeps the place the earlier one took. ofList takes literal keys; this one takes computed ones.

The same dictionary as Dict, declared to cross the boundary as a plain object rather than as a Map. Inside the module the two are one thing — a value of either is a Value.dict, and every operation runs on the same Map — so what the constructor decides is only what a consumer meets: JSON.stringify of a Map is {}, and what a consumer stringifies is a return value.

ofList writes one out key by key, and set and erase give back the spelling they were handed, so a declaration can build one as readily as it can be handed one.

Writing a key already present leaves it where it is; writing a new one appends.

How many entries, as the Int53 the subset counts in.

What k is bound to, or dflt where it is bound to nothing.

An array indexed by a key read off each element, at this spelling. Dict.ofPairs is the same over a Map.

The entry an encoded Dict carries for one of its own.

The keys survive the encoding untouched, which is what lets the entry check ask about the author's own dictionary rather than about the encoded one.