What this repository checks about itself and a user never builds #

Everything this repository checks about itself and a user does not: the compiler correctness proofs, the #guards, the axiom pins, and the example the artifact is generated from.

It is a target of its own because nothing else names it. lean2js imports a user's module at run time and this repository's example not at all, so without this the proofs would go unbuilt — and a build with nothing checked looks exactly like a build that passed.

No declaration of this repository rests on an axiom of its own #

Lean2Js/Axioms.lean pins the axioms of the theorems that ship as claims, which leaves every lemma no shipped claim reaches: a sorry in one of those is a warning lake build prints and nothing reads. The sweep below is this whole repository rather than the manifest's namespace, and it is here because this is the only module whose imports reach every other one.

A constant resting on an axiom rests on one that some constant on the way names directly, so reading the constants each declaration mentions catches a sorry written anywhere in this repository, without walking the dependency graph once per theorem.

What is swept is every declaration made by a module of this repository, rather than every name under the Lean2Js namespace: a private lemma is held under a name of its own that the namespace does not reach, and scaffolding lemmas here are private by convention.