JSON-like syntax for Lean.

Now you can write

open Std.Json

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

def Std.Json.jso.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.jso : Lean.Parser.Category

Json syntactic category

Equations

• Lean.Parser.Category.jso = { }

def Std.Json.jsoNull : Lean.ParserDescr

Json null value syntax.

Equations

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

def Std.Json.jsoTrue : Lean.ParserDescr

Json true value syntax.

Equations

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

def Std.Json.jsoFalse : Lean.ParserDescr

Json false value syntax.

Equations

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

def Std.Json.jso_ : Lean.ParserDescr

Json string syntax.

Equations

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

def Std.Json.«jso-_» : Lean.ParserDescr

Json number negation syntax for ordinary numbers.

Equations

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

def Std.Json.«jso-__1» : Lean.ParserDescr

Json number negation syntax for scientific numbers.

Equations

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

def Std.Json.«jso[_]» : Lean.ParserDescr

Json array syntax.

Equations

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

def Std.Json.jsoIdent : Lean.ParserDescr

Json identifier syntax.

Equations

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

def Std.Json.jsoField : Lean.ParserDescr

Json key/value syntax.

Equations

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

def Std.Json.«jso{_}» : Lean.ParserDescr

Json object syntax.

Equations

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

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

Allows to use Json syntax in a Lean file.

Equations

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