lean2js

Lean2Js.NodeCheck

source

Imports 3

Holding the artifact against the real JavaScript engine before it is written #

The script emit runs on Node against the package it is about to write, calling every vector on the real JavaScript engine. JsSem is Lean's picture of JavaScript; this is where the picture is held against the engine itself.

def

Lean2Js.nodeDisagreementMark

source
:
String

The words the check prints where it ran to a verdict and the vectors did not agree. emit reads them back out of what the script printed, which is how a module the engine disagreed with is told apart from a node that never reached the comparison at all.

Equations
Instances For
    Used by
      def

      Lean2Js.nodeCheckScript

      source
      :
      String

      A string rather than a .mjs file read by include_str: Lake does not track a file include_str reads, so an edit to it would leave the old script running until this module rebuilt for another reason.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Used by