JSON-like syntax for Lean.

Now you can write

open scoped ProofWidgets.Json

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

def ProofWidgets.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

Equations

• Lean.Parser.Category.jso = { }

instance ProofWidgets.Json.instOfScientificJsonNumber : OfScientific Lean.JsonNumber

Equations

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

instance ProofWidgets.Json.instNegJsonNumber : Neg Lean.JsonNumber

Equations

• ProofWidgets.Json.instNegJsonNumber = { neg := fun jn => { mantissa := -jn.mantissa, exponent := jn.exponent } }

instance ProofWidgets.Json.instToJsonFloat : Lean.ToJson Float

Equations

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

def ProofWidgets.Json.jsoNull : Lean.ParserDescr

Equations

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

def ProofWidgets.Json.jsoTrue : Lean.ParserDescr

Equations

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

def ProofWidgets.Json.jsoFalse : Lean.ParserDescr

Equations

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

def ProofWidgets.Json.jso_ : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def ProofWidgets.Json.jsoIdent : Lean.ParserDescr

Equations

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

def ProofWidgets.Json.jsoField : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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