The types that may sit on the boundary of the public API. Only those whose JS representation is uniquely determined are listed.

var stands for a type parameter and is only ever written inside the field types of the TypeDef that declares it; every type reaching a boundary has had its parameters substituted away.

option and result stay built in even though a user could now declare them, because the subset has literal syntax for their constructors and the generated runtime checks them by shape. Expressing them as declarations would remove neither special case.

Written out rather than derived so that Ty.eq_of_beq can be proved: Ty nests a List Ty, and neither DecidableEq nor LawfulBEq derives through that. Recursing through a list helper keeps it structural, so a type comparison still closes by rfl.

Written out for the reason Ty.beq is: a type comparison is what ties the knot in a recursive descriptor, and the knot has to be tied on equality rather than on a Bool nothing reads back.

A node count, used to bound how far a type can be expanded. sizeOf would say the same thing, but its derived instance is noncomputable and this number is computed while compiling.

Each argument carries its own leading space rather than being joined by one, so that a name applied to nothing renders as the bare name without a case split on the list.

Replaces a declaration's type parameters with the arguments it was applied to. Recursing through a list helper rather than args.map keeps this out of partial, which a proof about a declaration cannot unfold.

Whether a type's own shape reaches no dictObj. Written through a list helper rather than args.all for the reason Ty.beq is: a structural recursion is what a proof can unfold.

This says nothing about what a named type's fields hold — those come from the program, not from the type — so the reading a proof needs is this together with Program.noDictObj.

Substituting types that reach no dictObj into a type that reaches none leaves one that reaches none. This is what carries Ty.noDictObj through TypeDef.ctorsAt, which is the only place a field's type is read at a use of the type it belongs to.

The types a substitution puts in reach no dictObj when the arguments it was built from reach none. TypeDef.ctorsAt builds its substitution by zipping the declared parameters against them.

The string operations that take only the string. length is not here: an Array has one too, so the two share Expr.length.

all and any differ only in which answer ends the walk, so they share one form. find does not join them: it answers with the element rather than with a Bool.

What one match arm tests the scrutinee against. Nesting is what lets a rule branch on a combination — a state together with a role — instead of one constructor at a time, and a wildcard is what lets it name the combinations it cares about and leave the rest to a fallback.

bind and wild differ only in whether the value is given a name; the exhaustiveness check treats them alike.

For none and error / ok one side's type is not determined by the term, so the syntax carries an annotation.

The array combinators carry their binder and body rather than taking a function, so no value in the subset is ever a function.

How a fold carries one of a constructor's fields: the declared type coming round, a list of it coming round, or neither.

Which of a constructor's fields a fold over typeName tyArgs goes into, read off the field's own declared type. This is the one test: the evaluator walks by it and the emitter writes its spec from it, so the two cannot disagree about which field comes round.

Only the type at the same arguments comes round. Tree Int inside Tree String is a different type and a fold over one does not descend into the other.

A structure / inductive declared by the user. The single-constructor ones are the structures.

params names the type parameters that the field types may mention as Ty.var.

discriminator is the key the generated JavaScript tells this type's constructors apart by: tag unless the author wrote @[discriminator "..."] above the type.

The constructor names the subset spells itself, in Option and Result. No TypeDef declares them, so they are carried under tag and a declared type may not key one of them elsewhere.

Which key a constructor's name is carried under in the generated JavaScript.

A value the reference semantics returns carries the name of its constructor and not the type it came from, so the key that name is written with has to be decided by the name alone. The compiler and encodeValue both read it from here, which is what makes the two write the same object; Compile.validateType is what checks this reading against what each type declares.

The two laws are what the generated code needs of a key wherever it is written rather than read off a type, so they are carried here and not asked again at each use. Program.discriminators? is where a program's own reading is checked against them.

The constructors as seen by a use of the type at args. Every lookup that reads a field's type rather than its name goes through here; reading a name back does not need the substitution.

One pure function the package carries.

Whether the entry check has something to read in every parameter. A function value has no shape to check, so a declaration taking one has nothing to refuse at the boundary — which is what the refusing direction, the descent and the small-step agreement each ask for, and all they ask for. Named apart from isPublic because the two answer different questions and a proof wants this one.

A declaration crosses the boundary when its author meant it to and the entry check can read its parameters. A declaration that takes a function is internal whatever the author wrote: a function value cannot be checked at the boundary, so one that would need one checked never reaches it at all.

Whether a declared type's fields reach no dictObj, read before its parameters are substituted away. The substitution only ever puts in types the use site wrote, so reading it here is enough.

Whether a declaration's boundary reaches no dictObj.

Whether no type this program declares reaches a dictObj. This is the half encodeAt reads: it recurses into a declared type's fields and never into a declaration, so a program may hand a dictionary across as a plain object and still satisfy this.

Whether nothing this program declares crosses the boundary as a plain object.

Every claim written before a dictionary could cross as one holds under this, which is what lets those claims keep the exact text they have: encodeAt_eq_encodeValue carries them back to encodeValue rather than restating them.

A declaration's return type, where the program reaches no dictObj.

A declaration's parameter types, where the program reaches no dictObj.

Looks up the type a constructor name belongs to. match can reach the type definition from the scrutinee's type, so only the typing of ctor uses this.

The field types a constructor is read at, where no type the program declares reaches a dictObj and the type was used at arguments that reach none. This is the step encodeAt takes at a named type.

What a type's key has to be before a constructor's name can be read as carrying it.

Written as a recursion rather than forM so that the two readings below can be taken back out of it.

The reading this program declares: a constructor is carried under the key of the type that declares it, and under tag when no type does — which is Option and Result, whose constructors are the subset's own. Checked, because the reading is what the compiler and encodeValue share and the laws above are what the generated code needs of it.