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)
}

def Lean.Json.json.quot : Lean.ParserDescr

def Lean.Parser.Category.json : Lean.Parser.Category

Json syntactic category

Equations

• Lean.Parser.Category.json = { }

def Lean.Json.jsonNull : Lean.ParserDescr

Json null value syntax.

def Lean.Json.jsonTrue : Lean.ParserDescr

Json true value syntax.

Equations

• Lean.Json.jsonTrue = Lean.ParserDescr.node `Lean.Json.jsonTrue 1024 (Lean.ParserDescr.nonReservedSymbol "true" false)

def Lean.Json.jsonFalse : Lean.ParserDescr

Json false value syntax.

Equations

• Lean.Json.jsonFalse = Lean.ParserDescr.node `Lean.Json.jsonFalse 1024 (Lean.ParserDescr.nonReservedSymbol "false" false)

def Lean.Json.json_ : Lean.ParserDescr

Json string syntax.

Equations

• Lean.Json.json_ = Lean.ParserDescr.node `Lean.Json.json_ 1022 (Lean.ParserDescr.const `str)

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

Json number negation syntax for ordinary numbers.

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.

def Lean.Json.«json[_]» : Lean.ParserDescr

Json array syntax.

Equations

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

def Lean.Json.jsonIdent : Lean.ParserDescr

Json identifier syntax.

Equations

• Lean.Json.jsonIdent = Lean.ParserDescr.nodeWithAntiquot "jsonIdent" `Lean.Json.jsonIdent (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.const `str))

def Lean.Json.jsonField : Lean.ParserDescr

Json key/value syntax.

def Lean.Json.«json{_}» : Lean.ParserDescr

Json object syntax.

def Lean.Json.«termJson%_» : Lean.ParserDescr

Allows to use Json syntax in a Lean file.

Equations

• Lean.Json.«termJson%_» = Lean.ParserDescr.node `Lean.Json.«termJson%_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "json% ") (Lean.ParserDescr.cat `json 0))