Documentation

Lean.Data.Json.Elab

JSON-like syntax for Lean. #

Now you can write

open Lean.Json

#eval json% {
  hello : "world",
  cheese : ["edam", "cheddar", {kind : "spicy", rank : 100.2}],
  lemonCount : 100e30,
  isCool : true,
  isBug : null,
  lookACalc: $(23 + 54 * 2)
}

Json syntactic category

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

      Json null value syntax.

      Equations
      Instances For

        Json true value syntax.

        Equations
        Instances For

          Json false value syntax.

          Equations
          Instances For

            Json string syntax.

            Equations
            Instances For

              Json number negation syntax for ordinary numbers.

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

                Json number negation syntax for scientific numbers.

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

                  Json array syntax.

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

                    Json identifier syntax.

                    Equations
                    Instances For

                      Json key/value syntax.

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

                        Json object syntax.

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

                          Allows to use Json syntax in a Lean file.

                          Equations
                          Instances For