An author's theorem as a claim about the shipped JavaScript #

Lean2Js/Example.lean proves theorems about ordinary Lean functions. This is the descent: what one of those theorems says about the module the compiler writes.

The step that crosses is the certificate, which certificates% wrote next to the declaration. Everything else — that the generated function agrees with the reference semantics, that it throws the same codes, that arguments the entry refuses never reach the body — is proved once about every program and cited here without knowing what the declaration looks like.

What the walk refuses is pinned here too: a refusal is part of the subset's boundary, and a #guard_msgs is what keeps the wording from drifting.

The fold deriving Enc writes for a type that names itself #

A type that names itself has a walk over it, and the subset has no recursion to spell one with, so the walk has to be a name — and a name per type, because the algebra has one function per constructor. deriving Enc writes that name beside the encoding and marks it with the type it walks, so that the walk is found by the mark rather than by a suffix an author's own Category.fold would also carry.

Beside the fold it writes the alternatives a fold is reified to and the certificate that the subset's walk over them computes it. Reify reads all three where an author calls the fold, so what is pinned here is what that reading stands on.

The alternatives: one per constructor, in declaration order, every field bound. An author writes no match to fold, so there is no matcher to read them off — Reify writes them, and binding every field is what makes them exhaustive at every column the walk goes into.

And the two halves meeting, which is what a reified fold will be: the plumbing takes the scrutinee and a walk, deriving Enc wrote the walk for the type that has one, and the alternatives the walk was proved about are the ones Reify writes. Nothing here knows what the bodies are — only that each denotes its constructor's own function, which is what reifying the algebra's lambda hands over.

What the walk refuses #

A refusal that cannot name what to write instead names the rule the term broke, and the three rules are the three questions the subset reference opens with: what may be a value, how a program repeats, and whose vocabulary it reads. One fixture per rule is what keeps the two sides from drifting — the wording lives in Lean2Js.Reify and is read back here.

Lean's / on Int rounds towards negative infinity and the subset's truncates, so / is not a form the walk may quietly accept. It refuses at the reify_decl% call rather than at the author's /: Lean.Expr carries no source positions, so pointing at the author's own syntax needs more than the elaborated term.

A lambda is a value nowhere: the traversals carry their binder and body as syntax, and every other position wants a value the boundary can carry.

A type with no Enc has no place in Value, so there is nothing for the boundary to carry it as.

== is the one refusal about the type rather than about the term. eval compares encodings, so a type whose BEq is not known to decide equality has nothing to say about what that comparison means.

A call is the one refusal the author can act on, so it says which certificate was missing rather than that the term was unreadable.

A function crosses the boundary as a declaration's name, so a function the author wrote inline has no name to cross as.