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)
}
source
def Lean.Parser.Category.json :
Lean.Parser.Category

Json syntactic category

Equations
source
def Lean.Json.json.quot :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Json.jsonNull :
Lean.ParserDescr

Json null value syntax.

Equations
source
def Lean.Json.jsonTrue :
Lean.ParserDescr

Json true value syntax.

Equations
source
def Lean.Json.jsonFalse :
Lean.ParserDescr

Json false value syntax.

Equations
source
def Lean.Json.json_ :
Lean.ParserDescr

Json string syntax.

Equations
source
def Lean.Json.«json-_» :
Lean.ParserDescr

Json number negation syntax for ordinary numbers.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Json.«json-__1» :
Lean.ParserDescr

Json number negation syntax for scientific numbers.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Json.«json[_]» :
Lean.ParserDescr

Json array syntax.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Json.jsonIdent :
Lean.ParserDescr

Json identifier syntax.

Equations
source
def Lean.Json.jsonField :
Lean.ParserDescr

Json key/value syntax.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Json.«json{_}» :
Lean.ParserDescr

Json object syntax.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Json.«termJson%_» :
Lean.ParserDescr

Allows to use Json syntax in a Lean file.

Equations