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 : ParserDescr

Equations

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

def Lean.Parser.Category.json : Category

Json syntactic category

Equations

• Lean.Parser.Category.json = { }

def Lean.Json.jsonNull : ParserDescr

Json null value syntax.

Equations

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

def Lean.Json.jsonTrue : 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 : 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_ : ParserDescr

Json string syntax.

Equations

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

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

Json number negation syntax for ordinary numbers.

Equations

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

def Lean.Json.«json-__1» : 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[_]» : ParserDescr

Json array syntax.

Equations

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

def Lean.Json.jsonIdent : 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 : ParserDescr

Json key/value syntax.

Equations

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

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

Json object syntax.

Equations

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

def Lean.Json.«termJson%_» : 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))