w/ objects on ndjson lines
Initial metadata object:
{
"exporter": {
"name": string,
"version": string,
},
"lean": {
"version": string,
}
"num_names"?: integer,
"num_levels"?: integer,
"num_exprs"?: integer,
"num_declars"?: integer
}
Name.str
{
"str": {
"pre": integer,
"str": string
},
"i": integer,
}
Name.num
{
"num": {
"pre": integer,
"i": integer
}
"i": integer,
}
Level.succ
{
"succ": integer
"i": integer,
}
Level.max
{
"max": [integer, integer],
"i": integer,
}
Level.imax
{
"imax": [integer, integer],
"i": integer,
}
Level.param
{
"param": integer,
"i": integer,
}
Expr.bvar
{
"bvar": {
"deBrujinIndex": integer
}
"i": integer,
}
Expr.sort
{
"sort": {
"u": integer
}
"i": integer,
}
Expr.const
{
"const": {
"declName": integer,
"us": Array<integer>
}
"i": integer,
}
Expr.app
{
"app": {
"fn": number,
"arg": number
}
"i": integer,
}
Expr.lam
{
"lam": {
"binderName": integer,
"binderType": integer,
"body": integer,
"binderInfo": "default" | "implicit" | "strictImplicit" | "instImplicit"
}
"i": integer,
}
Expr.forallE
{
"forallE": {
"binderName": integer,
"binderType": integer,
"body": integer,
"binderInfo": "default" | "implicit" | "strictImplicit" | "instImplicit"
}
"i": integer,
}
Expr.letE
{
"letE": {
"declName": integer,
"type": integer,
"value": integer,
"body": integer,
"nondep": boolean
}
"i": integer,
}
Expr.proj
{
"proj": {
"typeName": integer,
"idx": integer,
"struct": integer
}
"i": integer,
}
Expr.lit (Literal.natVal)
{
"lit": {
"natVal": {
"val": integer
}
}
"i": integer,
}
Expr.lit (Literal.strVal)
{
"lit": {
"strVal": {
"val": string
}
}
"i": integer,
}
Expr.mdata
{
"mdata": {
"expr": integer,
"data": object
},
"i": integer
}
ConstantInfo.axiomInfo
{
"axiomInfo": {
"name": integer,
"levelParams": Array<integer>,
"type": integer,
"isUnsafe": boolean
}
}
ConstantInfo.defnInfo
{
"defnInfo": {
"name": integer,
"levelParams": Array<integer>,
"type": integer,
"value": integer,
"hints": Array<"opaque" | "abbrev" | integer>
"safety": "unsafe" | "safe" | "partial"
"all": Array<integer>
}
}
ConstantInfo.thmInfo
{
"thmInfo": {
"name": integer,
"levelParams": Array<integer>,
"type": integer,
"value": integer,
"all": Array<integer>
}
}
ConstantInfo.opaqueInfo
{
"opaqueInfo": {
"name": integer,
"levelParams": Array<integer>,
"type": integer,
"value": integer,
"isUnsafe": boolean,
"all": Array<integer>
}
}
ConstantInfo.quotInfo
{
"quotInfo": {
"name": integer,
"levelParams": Array<integer>,
"type": integer,
"kind": "type" | "ctor" | "lift" | "ind"
}
}
ConstantInfo.inductInfo
{
"inductInfo": {
"name": integer,
"levelParams": Array<integer>,
"type": integer,
"numParams": integer,
"numIndices": integer,
"all": Array<integer>,
"ctors": Array<integer>,
"numNested": integer,
"isRec": boolean,
"isUnsafe": boolean,
"isReflexive": boolean,
}
}
ConstantInfo.ctorInfo
{
"ctorInfo": {
"name": integer,
"levelParams": Array<integer>,
"type": integer,
"induct": integer,
"cidx": integer,
"numParams": integer,
"numFields": integer,
"isUnsafe": boolean
}
}
{
"RecursorRule": {
"ctor": integer,
"nfields": integer,
"rhs": integer
}
}
ConstantInfo.recInfo
{
"recInfo": {
"name": integer,
"levelParams": Array<integer>,
"type": integer,
"all": Array<integer>,
"numParams": integer,
"numIndices": integer,
"numMotives": integer,
"numMinors": integer,
"rules": Array<integer>,
"k": boolean,
"isUnsafe": boolean
}
}