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

def Lean.Parser.Category.json : Category

Json syntactic category

def Lean.Json.jsonNull : ParserDescr

Json null value syntax.

def Lean.Json.jsonTrue : ParserDescr

Json true value syntax.

def Lean.Json.jsonFalse : ParserDescr

Json false value syntax.

def Lean.Json.json_ : ParserDescr

Json string syntax.

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

Json number negation syntax for ordinary numbers.

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

Json number negation syntax for scientific numbers.

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

Json array syntax.

def Lean.Json.jsonIdent : ParserDescr

Json identifier syntax.

def Lean.Json.jsonField : ParserDescr

Json key/value syntax.

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

Json object syntax.

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

Allows to use Json syntax in a Lean file.