deriving Enc for the types an author declares #

An author's inductive or structure is not one of the types Lean2Js/Enc.lean knows, so where it sits inside Value has to be written when the type is. This is that, generated: the Core.TypeDef a program declares it as, the encoding and its inverse, and the entry check for the values the encoding produces.

Everything the handler emits is a top-level declaration rather than a field of the instance, so each proof is an ordinary equation-style definition over the constructors and the instance is the line that wires them together.

A type that names itself #

Enc answers for a type that is already there, and the type being declared is not, so a field whose type is that one cannot go through the class. Everything below writes such a field's half by hand; the halves that walk a list of the type sit in a mutual block with the ones that walk the type.

The certificate that the subset's walk computes the fold #

T.fold is written per type, so the theorem that the subset's walk computes it is too: denotes_foldE abstracts the walk and asks for that theorem as hw, and it is the one step of a fold's descent that cannot be proved once for every program.

What is generated is an induction over the type, in a mutual block with the List T half — the move ofValue_toValue / ofValues_map already makes. One constructor's case reads the node, then its fields left to right, then which alternative fires, and hands what is left to that constructor's own hypothesis. A field that comes round splits on whether its walk answered, so every step after it sits inside that split, which is why a case is assembled from its last field back.