Skip to content

Instantly share code, notes, and snippets.

@ammkrn

ammkrn/lean_export.schema.json

Created November 28, 2025 21:49
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save ammkrn/d68a78873c9e48e6ec4e971efc230a56 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save ammkrn/d68a78873c9e48e6ec4e971efc230a56 to your computer and use it in GitHub Desktop.
Download ZIP
lean_export.schema.json
Raw
lean_export.schema.json
{
"$schema": "http://json-schema.org/draft-07/schema#",
"oneOf": [
{
"type": "object",
"required": ["exporter", "lean"],
"properties": {
"exporter": {
"type": "object",
"required": ["name", "version"],
"properties": {
"name": { "type": "string" },
"version":{ "type": "string" }
}
},
"lean": {
"type": "object",
"required": ["version"],
"properties": {
"version": { "type": "string" }
}
},
"num_names": { "type": "integer" },
"num_levels": { "type": "integer" },
"num_exprs": { "type": "integer" },
"num_declars": { "type": "integer" }
}
},
{
"type": "object",
"required": ["str", "i"],
"properties": {
"str": {
"type": "object",
"required": ["pre", "str"],
"properties": {
"pre": { "type": "integer" },
"str": { "type": "string" }
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["num", "i"],
"properties": {
"num": {
"type": "object",
"required": ["pre", "i"],
"properties": {
"pre": { "type": "integer" },
"i": { "type": "integer" }
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["succ", "i"],
"properties": {
"succ": { "type": "integer" },
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["max", "i"],
"properties": {
"max": {
"type": "array",
"items": [
{ "type": "integer" },
{ "type": "integer" }
],
"minItems": 2,
"maxItems": 2
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["imax", "i"],
"properties": {
"imax": {
"type": "array",
"items": [
{ "type": "integer" },
{ "type": "integer" }
],
"minItems": 2,
"maxItems": 2
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["param", "i"],
"properties": {
"param": { "type": "integer" },
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["bvar", "i"],
"properties": {
"bvar": {
"type": "object",
"required": ["deBrujinIndex"],
"properties": {
"deBrujinIndex": { "type": "integer" }
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["sort", "i"],
"properties": {
"sort": {
"type": "object",
"required": ["u"],
"properties": {
"u": { "type": "integer" }
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["const", "i"],
"properties": {
"const": {
"type": "object",
"required": ["declName", "us"],
"properties": {
"declName": { "type": "integer" },
"us": {
"type": "array",
"items": { "type": "integer" }
}
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["app", "i"],
"properties": {
"app": {
"type": "object",
"required": ["fn", "arg"],
"properties": {
"fn": { "type": "number" },
"arg": { "type": "number" }
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["lam", "i"],
"properties": {
"lam": {
"type": "object",
"required": ["binderName", "binderType", "body", "binderInfo"],
"properties": {
"binderName": { "type": "integer" },
"binderType": { "type": "integer" },
"body": { "type": "integer" },
"binderInfo": {
"type": "string",
"enum": ["default", "implicit", "strictImplicit", "instImplicit"]
}
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["forallE", "i"],
"properties": {
"forallE": {
"type": "object",
"required": ["binderName", "binderType", "body", "binderInfo"],
"properties": {
"binderName": { "type": "integer" },
"binderType": { "type": "integer" },
"body": { "type": "integer" },
"binderInfo": {
"type": "string",
"enum": ["default", "implicit", "strictImplicit", "instImplicit"]
}
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["letE", "i"],
"properties": {
"letE": {
"type": "object",
"required": ["declName", "type", "value", "body", "nondep"],
"properties": {
"declName": { "type": "integer" },
"type": { "type": "integer" },
"value": { "type": "integer" },
"body": { "type": "integer" },
"nondep": { "type": "boolean" }
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["proj", "i"],
"properties": {
"proj": {
"type": "object",
"required": ["typeName", "idx", "struct"],
"properties": {
"typeName": { "type": "integer" },
"idx": { "type": "integer" },
"struct": { "type": "integer" }
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["lit", "i"],
"properties": {
"lit": {
"type": "object",
"required": ["natVal"],
"properties": {
"natVal": {
"type": "object",
"required": ["val"],
"properties": {
"val": { "type": "integer" }
}
}
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["lit", "i"],
"properties": {
"lit": {
"type": "object",
"required": ["strVal"],
"properties": {
"strVal": {
"type": "object",
"required": ["val"],
"properties": {
"val": { "type": "string" }
}
}
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["mdata", "i"],
"properties": {
"mdata": {
"type": "object",
"required": ["expr", "data"],
"properties": {
"expr": { "type": "integer" },
"data": { "type": "object" }
}
},
"i": { "type": "integer" }
}
},
{
"type": "object",
"required": ["axiomInfo"],
"properties": {
"axiomInfo": {
"type": "object",
"required": ["name", "levelParams", "type", "isUnsafe"],
"properties": {
"name": { "type": "integer" },
"levelParams": {
"type": "array",
"items": { "type": "integer" }
},
"type": { "type": "integer" },
"isUnsafe": { "type": "boolean" }
}
}
}
},
{
"type": "object",
"required": ["defnInfo"],
"properties": {
"defnInfo": {
"type": "object",
"required": [
"name",
"levelParams",
"type",
"value",
"hints",
"safety",
"all"
],
"properties": {
"name": { "type": "integer" },
"levelParams": {
"type": "array",
"items": { "type": "integer" }
},
"type": { "type": "integer" },
"value": { "type": "integer" },
"hints": {
"type": "array",
"items": {
"oneOf": [
{ "type": "integer" },
{
"type": "string",
"enum": ["opaque", "abbrev"]
}
]
}
},
"safety": {
"type": "string",
"enum": ["unsafe", "safe", "partial"]
},
"all": {
"type": "array",
"items": { "type": "integer" }
}
}
}
}
},
{
"type": "object",
"required": ["thmInfo"],
"properties": {
"thmInfo": {
"type": "object",
"required": ["name", "levelParams", "type", "value", "all"],
"properties": {
"name": { "type": "integer" },
"levelParams": {
"type": "array",
"items": { "type": "integer" }
},
"type": { "type": "integer" },
"value": { "type": "integer" },
"all": {
"type": "array",
"items": { "type": "integer" }
}
}
}
}
},
{
"type": "object",
"required": ["opaqueInfo"],
"properties": {
"opaqueInfo": {
"type": "object",
"required": [
"name",
"levelParams",
"type",
"value",
"isUnsafe",
"all"
],
"properties": {
"name": { "type": "integer" },
"levelParams": {
"type": "array",
"items": { "type": "integer" }
},
"type": { "type": "integer" },
"value": { "type": "integer" },
"isUnsafe": { "type": "boolean" },
"all": {
"type": "array",
"items": { "type": "integer" }
}
}
}
}
},
{
"type": "object",
"required": ["quotInfo"],
"properties": {
"quotInfo": {
"type": "object",
"required": ["name", "levelParams", "type", "kind"],
"properties": {
"name": { "type": "integer" },
"levelParams": {
"type": "array",
"items": { "type": "integer" }
},
"type": { "type": "integer" },
"kind": {
"type": "string",
"enum": ["type", "ctor", "lift", "ind"]
}
}
}
}
},
{
"type": "object",
"required": ["inductInfo"],
"properties": {
"inductInfo": {
"type": "object",
"required": [
"name",
"levelParams",
"type",
"numParams",
"numIndices",
"all",
"ctors",
"numNested",
"isRec",
"isUnsafe",
"isReflexive"
],
"properties": {
"name": { "type": "integer" },
"levelParams": {
"type": "array",
"items": { "type": "integer" }
},
"type": { "type": "integer" },
"numParams": { "type": "integer" },
"numIndices": { "type": "integer" },
"all": {
"type": "array",
"items": { "type": "integer" }
},
"ctors": {
"type": "array",
"items": { "type": "integer" }
},
"numNested": { "type": "integer" },
"isRec": { "type": "boolean" },
"isUnsafe": { "type": "boolean" },
"isReflexive": { "type": "boolean" }
}
}
}
},
{
"type": "object",
"required": ["ctorInfo"],
"properties": {
"ctorInfo": {
"type": "object",
"required": [
"name",
"levelParams",
"type",
"induct",
"cidx",
"numParams",
"numFields",
"isUnsafe"
],
"properties": {
"name": { "type": "integer" },
"levelParams": {
"type": "array",
"items": { "type": "integer" }
},
"type": { "type": "integer" },
"induct": { "type": "integer" },
"cidx": { "type": "integer" },
"numParams": { "type": "integer" },
"numFields": { "type": "integer" },
"isUnsafe": { "type": "boolean" }
}
}
}
},
{
"type": "object",
"required": ["RecursorRule"],
"properties": {
"RecursorRule": {
"type": "object",
"required": ["ctor", "nfields", "rhs"],
"properties": {
"ctor": { "type": "integer" },
"nfields": { "type": "integer" },
"rhs": { "type": "integer" }
}
}
}
},
{
"type": "object",
"required": ["recInfo"],
"properties": {
"recInfo": {
"type": "object",
"required": [
"name",
"levelParams",
"type",
"all",
"numParams",
"numIndices",
"numMotives",
"numMinors",
"rules",
"k",
"isUnsafe"
],
"properties": {
"name": { "type": "integer" },
"levelParams": {
"type": "array",
"items": { "type": "integer" }
},
"type": { "type": "integer" },
"all": {
"type": "array",
"items": { "type": "integer" }
},
"numParams": { "type": "integer" },
"numIndices": { "type": "integer" },
"numMotives": { "type": "integer" },
"numMinors": { "type": "integer" },
"rules": {
"type": "array",
"items": { "type": "integer" }
},
"k": { "type": "boolean" },
"isUnsafe": { "type": "boolean" }
}
}
}
}
]
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment