lean2js

Lean2Js.Json

source

Imports 2

A minimal JSON writer for the proof manifest and the test vectors #

A minimal JSON writer for emitting the proof manifest and the differential test vectors.

Lean.Json is avoided to keep the dependency on the Lean frontend out of the compiler proper (all this library then needs is IO.FS).

inductive

Lean2Js.Json

source
:
Type
Instances For
    Used by
      instance

      Lean2Js.instInhabitedJson

      source
      @[instance_reducible]
      :
      Inhabited Json
      Equations
      Used by
        partial def

        Lean2Js.Json.render

        source
        :
        Json → String
        Used by
          partial def

          Lean2Js.Json.renderPretty

          source
          (j : Json) (indent : String := "") :
          String

          Human-readable formatting. The artifact goes into git, so it is written out in a shape whose diff can be reviewed.

          Used by