The programs the compiler must not accept #

Pins down the programs the compiler must not accept.

The differential test only looks at "a program that got through returns the same answer in JS too". That what must not get through does not get through can only be checked on this side.

What a fold's alternatives are read at #

A fold's alternatives are matched against the rebuilt node, whose fields that came round carry the answers for them. Reading them at the declared type instead is not conservative: two types may declare constructors of the same name, so alternatives that name every head the declared type has can still leave a rebuilt node uncovered. Tree and Twig are that pair.

The shapes deriving Enc writes a fold's certificate for #

The certificate is generated per type, so a shape no type here declares has nothing else checking that the generator reaches it. Example.Category carries a plain field and a list of the type coming round; a constructor with no fields, a field that is the type itself, and both of those in one constructor are here. Nothing reads these types: that deriving Enc writes their fold, their alternatives and their certificate at all is what they pin.

And what a shipped def does with them. Example.Category is the only fold the example ships and it carries neither a constructor with no fields nor a field that is the type itself, so these are what say the walk reads those two: a constructor with no fields is handed a plain expression where the others are handed a lambda, and a field that came round arrives as the answer for it. ship_package is what makes that a check rather than an elaboration — it reifies each declaration, writes its certificate, compiles it and asks the fuel ceiling.

The key a type's constructors are told apart by #

tag unless the author wrote @[discriminator "..."] above the type. What a type declares has to be a name the generated code can write and has to stay free as a field name; and because a value carries its constructor's name and not the type it came from, the key has to follow the name — two types cannot key one name two ways, and the subset's own Option and Result constructors stay under tag.

What the string readers refuse #

Str.toInt? and Str.indexOf? carry their acceptance set in their own answers rather than in the compiler's tables, so without these the only place it is pinned is the emitted vectors.

Where Str.join puts the separator #

One separator between neighbours and none at either end, which the empty list and the one-element list are what pin down.

What Str.repeat does with a count it cannot honour #

A count of zero or less answers rather than trapping, the way Str.split on the empty separator answers. The trap is on the length of the result, and applyStrBin is where it lives.

How Str.padStart fills a width #

The pad is cut where the width falls, so a multi-character pad does not overshoot it. A width the string already reaches, and an empty pad, leave the string alone.

What bounds a result a value sizes #

Str.repeat and Arr.range are the two results whose size a value decides, and eval, the model of the JS and the JSON handed to Node each hold that result whole. Bound.programBounded is where the deciding value has to be bounded by the program text; these are the shapes either side of that line. A clamp reads through a let, and a binder that shadows the clamped name stops it. A length is not a bound: nothing in the text says how long the array a caller passes is.

A traversal runs its body once per element, so what the ceiling is measured against is the product. Only a traversal the text says the length of multiplies: an array a caller passes is as long as the vector generator made it.

Gathering a program #

program% reads the declarations out of the namespace, so the order the defs are written in is not the order they ship in: a callee moves ahead of its caller, and a declaration handed over as a function moves ahead of the callee it is handed to. A cycle cannot be written at all — Lean turns the defs away first — so what the compiler does with one is pinned above, on declarations built by hand.

What the @throws line names #

The codes are read off the body: each operation contributes what its case in eval can return, a call contributes its callee's, and a declaration handed over as a function contributes its own at the call that hands it over. That last one is why a call through a function-typed parameter adds nothing — the caller already counted it by naming the declaration. typeError is the entry check, so a declaration that takes no arguments does not carry it.

What reaches the .d.ts #

A declared type is printed only where a consumer can name it: from the signature of a public function, or through the fields of a type already reachable that way. A type that only ever holds an intermediate value -- the accumulator a foldl carries -- is in no public signature, and printing it would invite a consumer to build one.

The calendar answers what a calendar answers #

Cal is arithmetic with no special case in it, which is what lets it be in the subset — and also what means a transposed constant is wrong everywhere rather than at a boundary. The round trip is what says the two directions are inverse over a stretch holding four centuries, every leap rule and both sides of the epoch; the named days are what says the count is anchored where a reader thinks it is. These live here rather than beside the definitions because they are a user's build to run otherwise.