Verso Docstring Serialization

Verso docstrings (VersoDocString) contain a tree of Doc.Block/Doc.Inline nodes, which can include extension points (ElabInline/ElabBlock) which are opaque Dynamic values identified by Name. Different Lean packages can register their own extension types, so we can't know all possible types ahead of time.

The serialization strategy is:

• For each ElabInline/ElabBlock, look up a handler by name in DocstringValues.
• If a handler exists, serialize the payload with it. On deserialization, the same handler reconstructs the value.
• If no handler exists (the extension type is unknown), serialize just the name (tag byte 0). On deserialization, unknown extensions are replaced with an Unknown sentinel value and their payload bytes are skipped. This means the database remains readable even if extension types are not available to a client. In Verso docstrings, the content underneath a custom inline or block node represents an alternative “plain” representation, such as a generic code element instead of semantically-highlighted Lean code.

builtinDocstringValues (defined at the bottom of this file) registers the handlers for extension types that ship with Lean. If a downstream package defines custom Verso extensions, it would need to provide its own DocstringValues with additional handlers. There's presently no API for this, but the code is designed to allow plugins that provide handlers in the future.

structure DocGen4.DB.DocstringDataHandler : Type

Serializer/deserializer pair for a single Verso extension type.

• serialize : SQLite.Blob.Serializer Dynamic
• deserialize : SQLite.Blob.Deserializer Dynamic

structure DocGen4.DB.DocstringValues : Type

Registry of known Verso extension types, keyed by Name.

• handlers : Lean.NameMap DocstringDataHandler

def DocGen4.DB.toBinaryElabInline (vals : DocstringValues) : SQLite.Blob.Serializer Lean.ElabInline

Equations

• DocGen4.DB.toBinaryElabInline vals { name := name, val := val } x✝ = DocGen4.DB.toBinaryElab✝ vals name val x✝

def DocGen4.DB.toBinaryElabBlock (vals : DocstringValues) : SQLite.Blob.Serializer Lean.ElabBlock

Equations

• DocGen4.DB.toBinaryElabBlock vals { name := name, val := val } x✝ = DocGen4.DB.toBinaryElab✝ vals name val x✝

structure DocGen4.DB.Unknown : Type

@[implicit_reducible]

instance DocGen4.DB.instBEqUnknown : BEq Unknown

Equations

• DocGen4.DB.instBEqUnknown = { beq := DocGen4.DB.instBEqUnknown.beq }

def DocGen4.DB.instBEqUnknown.beq : Unknown → Unknown → Bool

Equations

• DocGen4.DB.instBEqUnknown.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance DocGen4.DB.instHashableUnknown : Hashable Unknown

Equations

• DocGen4.DB.instHashableUnknown = { hash := DocGen4.DB.instHashableUnknown.hash }

def DocGen4.DB.instHashableUnknown.hash : Unknown → UInt64

Equations

• DocGen4.DB.instHashableUnknown.hash { } = 0

@[implicit_reducible]

instance DocGen4.DB.instOrdUnknown : Ord Unknown

Equations

• DocGen4.DB.instOrdUnknown = { compare := DocGen4.DB.instOrdUnknown.ord }

def DocGen4.DB.instOrdUnknown.ord : Unknown → Unknown → Ordering

Equations

• DocGen4.DB.instOrdUnknown.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[implicit_reducible]

instance DocGen4.DB.instDecidableEqUnknown : DecidableEq Unknown

Equations

• DocGen4.DB.instDecidableEqUnknown x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance DocGen4.DB.instInhabitedUnknown : Inhabited Unknown

Equations

• DocGen4.DB.instInhabitedUnknown = { default := DocGen4.DB.instInhabitedUnknown.default }

@[implicit_reducible]

instance DocGen4.DB.instTypeNameUnknown : TypeName Unknown

Equations

• DocGen4.DB.instTypeNameUnknown = DocGen4.DB.inst✝

instance DocGen4.DB.instSubsingletonUnknown : Subsingleton Unknown

def DocGen4.DB.fromBinaryElabInline (vals : DocstringValues) : SQLite.Blob.Deserializer Lean.ElabInline

Equations

• DocGen4.DB.fromBinaryElabInline vals = do let __discr ← DocGen4.DB.fromBinaryElab✝ vals "ElabInline" match __discr with | (name, val) => pure { name := name, val := val }

def DocGen4.DB.fromBinaryElabBlock (vals : DocstringValues) : SQLite.Blob.Deserializer Lean.ElabBlock

Equations

• DocGen4.DB.fromBinaryElabBlock vals = do let __discr ← DocGen4.DB.fromBinaryElab✝ vals "ElabBlock" match __discr with | (name, val) => pure { name := name, val := val }

@[implicit_reducible]

instance DocGen4.DB.instToBinaryInline_docGen4 {i : Type u_1} [SQLite.Blob.ToBinary i] : SQLite.Blob.ToBinary (Lean.Doc.Inline i)

Equations

• DocGen4.DB.instToBinaryInline_docGen4 = { serializer := DocGen4.DB.instToBinaryInline_docGen4.go }

partial def DocGen4.DB.instToBinaryInline_docGen4.go {i : Type u_1} [SQLite.Blob.ToBinary i] : Lean.Doc.Inline i → ByteArray → ByteArray

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryInline_docGen4 {i : Type} [SQLite.Blob.FromBinary i] : SQLite.Blob.FromBinary (Lean.Doc.Inline i)

Equations

• DocGen4.DB.instFromBinaryInline_docGen4 = { deserializer := DocGen4.DB.instFromBinaryInline_docGen4.go }

partial def DocGen4.DB.instFromBinaryInline_docGen4.go {i : Type} [SQLite.Blob.FromBinary i] : SQLite.Blob.Deserializer (Lean.Doc.Inline i)

@[implicit_reducible]

instance DocGen4.DB.instToBinaryBlock_docGen4 {i : Type u_1} {b : Type u_2} [SQLite.Blob.ToBinary i] [SQLite.Blob.ToBinary b] : SQLite.Blob.ToBinary (Lean.Doc.Block i b)

Equations

• DocGen4.DB.instToBinaryBlock_docGen4 = { serializer := DocGen4.DB.instToBinaryBlock_docGen4.go }

partial def DocGen4.DB.instToBinaryBlock_docGen4.go {i : Type u_1} {b : Type u_2} [SQLite.Blob.ToBinary i] [SQLite.Blob.ToBinary b] : Lean.Doc.Block i b → ByteArray → ByteArray

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryBlock_docGen4 {i b : Type} [SQLite.Blob.FromBinary i] [SQLite.Blob.FromBinary b] : SQLite.Blob.FromBinary (Lean.Doc.Block i b)

Equations

• DocGen4.DB.instFromBinaryBlock_docGen4 = { deserializer := DocGen4.DB.instFromBinaryBlock_docGen4.go }

partial def DocGen4.DB.instFromBinaryBlock_docGen4.go {i b : Type} [SQLite.Blob.FromBinary i] [SQLite.Blob.FromBinary b] : SQLite.Blob.Deserializer (Lean.Doc.Block i b)

@[implicit_reducible]

instance DocGen4.DB.instToBinaryPart_docGen4 {i : Type u_1} {b : Type u_2} {p : Type u_3} [SQLite.Blob.ToBinary i] [SQLite.Blob.ToBinary b] [SQLite.Blob.ToBinary p] : SQLite.Blob.ToBinary (Lean.Doc.Part i p b)

Equations

• DocGen4.DB.instToBinaryPart_docGen4 = { serializer := DocGen4.DB.instToBinaryPart_docGen4.go }

partial def DocGen4.DB.instToBinaryPart_docGen4.go {i : Type u_1} {b : Type u_2} {p : Type u_3} [SQLite.Blob.ToBinary i] [SQLite.Blob.ToBinary b] [SQLite.Blob.ToBinary p] : Lean.Doc.Part i p b → ByteArray → ByteArray

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryPart_docGen4 {i b p : Type} [SQLite.Blob.FromBinary i] [SQLite.Blob.FromBinary b] [SQLite.Blob.FromBinary p] : SQLite.Blob.FromBinary (Lean.Doc.Part i p b)

Equations

• DocGen4.DB.instFromBinaryPart_docGen4 = { deserializer := DocGen4.DB.instFromBinaryPart_docGen4.go }

partial def DocGen4.DB.instFromBinaryPart_docGen4.go {i b p : Type} [SQLite.Blob.FromBinary i] [SQLite.Blob.FromBinary b] [SQLite.Blob.FromBinary p] : SQLite.Blob.Deserializer (Lean.Doc.Part i p b)

@[implicit_reducible]

def DocGen4.DB.versoDocStringToBinary (values : DocstringValues) : SQLite.Blob.ToBinary Lean.VersoDocString

Equations

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

@[implicit_reducible]

def DocGen4.DB.versoDocStringFromBinary (values : DocstringValues) : SQLite.Blob.FromBinary Lean.VersoDocString

Equations

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

@[implicit_reducible]

def DocGen4.DB.versoDocStringQueryParam (values : DocstringValues) : SQLite.QueryParam Lean.VersoDocString

Equations

• DocGen4.DB.versoDocStringQueryParam values = SQLite.QueryParam.asBlob

Builtin Data.* handlers

@[implicit_reducible]

instance DocGen4.DB.instToBinaryPreresolved_docGen4 : SQLite.Blob.ToBinary Lean.Syntax.Preresolved

Equations

• DocGen4.DB.instToBinaryPreresolved_docGen4 = { serializer := DocGen4.DB.instToBinaryPreresolved_docGen4.toBinaryAux }

def DocGen4.DB.instToBinaryPreresolved_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Syntax.Preresolved

Equations

• One or more equations did not get rendered due to their size.
• DocGen4.DB.instToBinaryPreresolved_docGen4.toBinaryAux (Lean.Syntax.Preresolved.namespace f_0) x✝ = SQLite.Blob.ToBinary.serializer f_0 (SQLite.Blob.ToBinary.serializer 0 x✝)

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryPreresolved_docGen4 : SQLite.Blob.FromBinary Lean.Syntax.Preresolved

Equations

• DocGen4.DB.instFromBinaryPreresolved_docGen4 = { deserializer := DocGen4.DB.instFromBinaryPreresolved_docGen4.fromBinaryAux }

def DocGen4.DB.instFromBinaryPreresolved_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Syntax.Preresolved

Equations

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

@[implicit_reducible]

instance DocGen4.DB.instToBinarySyntax_docGen4 : SQLite.Blob.ToBinary Lean.Syntax

Equations

• DocGen4.DB.instToBinarySyntax_docGen4 = { serializer := DocGen4.DB.instToBinarySyntax_docGen4.toBinaryAux }

partial def DocGen4.DB.instToBinarySyntax_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Syntax

@[implicit_reducible]

instance DocGen4.DB.instFromBinarySyntax_docGen4 : SQLite.Blob.FromBinary Lean.Syntax

Equations

• DocGen4.DB.instFromBinarySyntax_docGen4 = { deserializer := DocGen4.DB.instFromBinarySyntax_docGen4.fromBinaryAux }

partial def DocGen4.DB.instFromBinarySyntax_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Syntax

@[implicit_reducible]

instance DocGen4.DB.instToBinaryDataValue_docGen4 : SQLite.Blob.ToBinary Lean.DataValue

Equations

• DocGen4.DB.instToBinaryDataValue_docGen4 = { serializer := DocGen4.DB.instToBinaryDataValue_docGen4.toBinaryAux }

def DocGen4.DB.instToBinaryDataValue_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.DataValue

Equations

• DocGen4.DB.instToBinaryDataValue_docGen4.toBinaryAux (Lean.DataValue.ofString f_0) x✝ = SQLite.Blob.ToBinary.serializer f_0 (SQLite.Blob.ToBinary.serializer 0 x✝)
• DocGen4.DB.instToBinaryDataValue_docGen4.toBinaryAux (Lean.DataValue.ofBool f_0) x✝ = SQLite.Blob.ToBinary.serializer f_0 (SQLite.Blob.ToBinary.serializer 1 x✝)
• DocGen4.DB.instToBinaryDataValue_docGen4.toBinaryAux (Lean.DataValue.ofName f_0) x✝ = SQLite.Blob.ToBinary.serializer f_0 (SQLite.Blob.ToBinary.serializer 2 x✝)
• DocGen4.DB.instToBinaryDataValue_docGen4.toBinaryAux (Lean.DataValue.ofNat f_0) x✝ = SQLite.Blob.ToBinary.serializer f_0 (SQLite.Blob.ToBinary.serializer 3 x✝)
• DocGen4.DB.instToBinaryDataValue_docGen4.toBinaryAux (Lean.DataValue.ofInt f_0) x✝ = SQLite.Blob.ToBinary.serializer f_0 (SQLite.Blob.ToBinary.serializer 4 x✝)
• DocGen4.DB.instToBinaryDataValue_docGen4.toBinaryAux (Lean.DataValue.ofSyntax f_0) x✝ = SQLite.Blob.ToBinary.serializer f_0 (SQLite.Blob.ToBinary.serializer 5 x✝)

def DocGen4.DB.instFromBinaryDataValue_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.DataValue

Equations

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

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryDataValue_docGen4 : SQLite.Blob.FromBinary Lean.DataValue

Equations

• DocGen4.DB.instFromBinaryDataValue_docGen4 = { deserializer := DocGen4.DB.instFromBinaryDataValue_docGen4.fromBinaryAux }

def DocGen4.DB.instToBinaryKVMap_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.KVMap

Equations

• DocGen4.DB.instToBinaryKVMap_docGen4.toBinaryAux { entries := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instToBinaryKVMap_docGen4 : SQLite.Blob.ToBinary Lean.KVMap

Equations

• DocGen4.DB.instToBinaryKVMap_docGen4 = { serializer := DocGen4.DB.instToBinaryKVMap_docGen4.toBinaryAux }

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryKVMap_docGen4 : SQLite.Blob.FromBinary Lean.KVMap

Equations

• DocGen4.DB.instFromBinaryKVMap_docGen4 = { deserializer := DocGen4.DB.instFromBinaryKVMap_docGen4.fromBinaryAux }

def DocGen4.DB.instFromBinaryKVMap_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.KVMap

Equations

• DocGen4.DB.instFromBinaryKVMap_docGen4.fromBinaryAux = (fun (f_0 : List (Lean.Name × Lean.DataValue)) => { entries := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instToBinaryExpr_docGen4 : SQLite.Blob.ToBinary Lean.Expr

Equations

• DocGen4.DB.instToBinaryExpr_docGen4 = { serializer := DocGen4.DB.instToBinaryExpr_docGen4.toBinaryAux }

partial def DocGen4.DB.instToBinaryExpr_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Expr

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryExpr_docGen4 : SQLite.Blob.FromBinary Lean.Expr

Equations

• DocGen4.DB.instFromBinaryExpr_docGen4 = { deserializer := DocGen4.DB.instFromBinaryExpr_docGen4.fromBinaryAux }

partial def DocGen4.DB.instFromBinaryExpr_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Expr

def DocGen4.DB.instToBinaryDocHighlight_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.DocHighlight

Equations

• One or more equations did not get rendered due to their size.
• DocGen4.DB.instToBinaryDocHighlight_docGen4.toBinaryAux Lean.Doc.DocHighlight.keyword x✝ = SQLite.Blob.ToBinary.serializer 4 x✝

@[implicit_reducible]

instance DocGen4.DB.instToBinaryDocHighlight_docGen4 : SQLite.Blob.ToBinary Lean.Doc.DocHighlight

Equations

• DocGen4.DB.instToBinaryDocHighlight_docGen4 = { serializer := DocGen4.DB.instToBinaryDocHighlight_docGen4.toBinaryAux }

def DocGen4.DB.instFromBinaryDocHighlight_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.DocHighlight

Equations

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

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryDocHighlight_docGen4 : SQLite.Blob.FromBinary Lean.Doc.DocHighlight

Equations

• DocGen4.DB.instFromBinaryDocHighlight_docGen4 = { deserializer := DocGen4.DB.instFromBinaryDocHighlight_docGen4.fromBinaryAux }

def DocGen4.DB.instToBinaryDocCode_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.DocCode

Equations

• DocGen4.DB.instToBinaryDocCode_docGen4.toBinaryAux { code := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instToBinaryDocCode_docGen4 : SQLite.Blob.ToBinary Lean.Doc.DocCode

Equations

• DocGen4.DB.instToBinaryDocCode_docGen4 = { serializer := DocGen4.DB.instToBinaryDocCode_docGen4.toBinaryAux }

def DocGen4.DB.instFromBinaryDocCode_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.DocCode

Equations

• DocGen4.DB.instFromBinaryDocCode_docGen4.fromBinaryAux = (fun (f_0 : Array (String × Option Lean.Doc.DocHighlight)) => { code := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryDocCode_docGen4 : SQLite.Blob.FromBinary Lean.Doc.DocCode

Equations

• DocGen4.DB.instFromBinaryDocCode_docGen4 = { deserializer := DocGen4.DB.instFromBinaryDocCode_docGen4.fromBinaryAux }

@[implicit_reducible]

instance DocGen4.DB.instToBinaryConst_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.Const

Equations

• DocGen4.DB.instToBinaryConst_docGen4 = { serializer := DocGen4.DB.instToBinaryConst_docGen4.toBinaryAux }

def DocGen4.DB.instToBinaryConst_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.Const

Equations

• DocGen4.DB.instToBinaryConst_docGen4.toBinaryAux { name := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryConst_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.Const

Equations

• DocGen4.DB.instFromBinaryConst_docGen4 = { deserializer := DocGen4.DB.instFromBinaryConst_docGen4.fromBinaryAux }

def DocGen4.DB.instFromBinaryConst_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.Const

Equations

• DocGen4.DB.instFromBinaryConst_docGen4.fromBinaryAux = (fun (f_0 : Lean.Name) => { name := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

def DocGen4.DB.instToBinaryTactic_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.Tactic

Equations

• DocGen4.DB.instToBinaryTactic_docGen4.toBinaryAux { name := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instToBinaryTactic_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.Tactic

Equations

• DocGen4.DB.instToBinaryTactic_docGen4 = { serializer := DocGen4.DB.instToBinaryTactic_docGen4.toBinaryAux }

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryTactic_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.Tactic

Equations

• DocGen4.DB.instFromBinaryTactic_docGen4 = { deserializer := DocGen4.DB.instFromBinaryTactic_docGen4.fromBinaryAux }

def DocGen4.DB.instFromBinaryTactic_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.Tactic

Equations

• DocGen4.DB.instFromBinaryTactic_docGen4.fromBinaryAux = (fun (f_0 : Lean.Name) => { name := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instToBinaryConvTactic_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.ConvTactic

Equations

• DocGen4.DB.instToBinaryConvTactic_docGen4 = { serializer := DocGen4.DB.instToBinaryConvTactic_docGen4.toBinaryAux }

def DocGen4.DB.instToBinaryConvTactic_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.ConvTactic

Equations

• DocGen4.DB.instToBinaryConvTactic_docGen4.toBinaryAux { name := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryConvTactic_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.ConvTactic

Equations

• DocGen4.DB.instFromBinaryConvTactic_docGen4 = { deserializer := DocGen4.DB.instFromBinaryConvTactic_docGen4.fromBinaryAux }

def DocGen4.DB.instFromBinaryConvTactic_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.ConvTactic

Equations

• DocGen4.DB.instFromBinaryConvTactic_docGen4.fromBinaryAux = (fun (f_0 : Lean.Name) => { name := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instToBinarySyntaxCat_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.SyntaxCat

Equations

• DocGen4.DB.instToBinarySyntaxCat_docGen4 = { serializer := DocGen4.DB.instToBinarySyntaxCat_docGen4.toBinaryAux }

def DocGen4.DB.instToBinarySyntaxCat_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.SyntaxCat

Equations

• DocGen4.DB.instToBinarySyntaxCat_docGen4.toBinaryAux { name := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

def DocGen4.DB.instFromBinarySyntaxCat_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.SyntaxCat

Equations

• DocGen4.DB.instFromBinarySyntaxCat_docGen4.fromBinaryAux = (fun (f_0 : Lean.Name) => { name := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instFromBinarySyntaxCat_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.SyntaxCat

Equations

• DocGen4.DB.instFromBinarySyntaxCat_docGen4 = { deserializer := DocGen4.DB.instFromBinarySyntaxCat_docGen4.fromBinaryAux }

def DocGen4.DB.instToBinaryModuleName_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.ModuleName

Equations

• DocGen4.DB.instToBinaryModuleName_docGen4.toBinaryAux { module := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instToBinaryModuleName_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.ModuleName

Equations

• DocGen4.DB.instToBinaryModuleName_docGen4 = { serializer := DocGen4.DB.instToBinaryModuleName_docGen4.toBinaryAux }

def DocGen4.DB.instFromBinaryModuleName_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.ModuleName

Equations

• DocGen4.DB.instFromBinaryModuleName_docGen4.fromBinaryAux = (fun (f_0 : Lean.Name) => { module := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryModuleName_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.ModuleName

Equations

• DocGen4.DB.instFromBinaryModuleName_docGen4 = { deserializer := DocGen4.DB.instFromBinaryModuleName_docGen4.fromBinaryAux }

@[implicit_reducible]

instance DocGen4.DB.instToBinaryOption_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.Option

Equations

• DocGen4.DB.instToBinaryOption_docGen4 = { serializer := DocGen4.DB.instToBinaryOption_docGen4.toBinaryAux }

def DocGen4.DB.instToBinaryOption_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.Option

Equations

• DocGen4.DB.instToBinaryOption_docGen4.toBinaryAux { name := f_0, declName := f_1 } x✝ = SQLite.Blob.ToBinary.serializer f_1 (SQLite.Blob.ToBinary.serializer f_0 x✝)

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryOption_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.Option

Equations

• DocGen4.DB.instFromBinaryOption_docGen4 = { deserializer := DocGen4.DB.instFromBinaryOption_docGen4.fromBinaryAux }

def DocGen4.DB.instFromBinaryOption_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.Option

Equations

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

def DocGen4.DB.instToBinaryAttributes_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.Attributes

Equations

• DocGen4.DB.instToBinaryAttributes_docGen4.toBinaryAux { stx := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instToBinaryAttributes_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.Attributes

Equations

• DocGen4.DB.instToBinaryAttributes_docGen4 = { serializer := DocGen4.DB.instToBinaryAttributes_docGen4.toBinaryAux }

def DocGen4.DB.instFromBinaryAttributes_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.Attributes

Equations

• DocGen4.DB.instFromBinaryAttributes_docGen4.fromBinaryAux = (fun (f_0 : Lean.Syntax) => { stx := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryAttributes_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.Attributes

Equations

• DocGen4.DB.instFromBinaryAttributes_docGen4 = { deserializer := DocGen4.DB.instFromBinaryAttributes_docGen4.fromBinaryAux }

@[implicit_reducible]

instance DocGen4.DB.instToBinaryAttribute_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.Attribute

Equations

• DocGen4.DB.instToBinaryAttribute_docGen4 = { serializer := DocGen4.DB.instToBinaryAttribute_docGen4.toBinaryAux }

def DocGen4.DB.instToBinaryAttribute_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.Attribute

Equations

• DocGen4.DB.instToBinaryAttribute_docGen4.toBinaryAux { stx := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryAttribute_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.Attribute

Equations

• DocGen4.DB.instFromBinaryAttribute_docGen4 = { deserializer := DocGen4.DB.instFromBinaryAttribute_docGen4.fromBinaryAux }

def DocGen4.DB.instFromBinaryAttribute_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.Attribute

Equations

• DocGen4.DB.instFromBinaryAttribute_docGen4.fromBinaryAux = (fun (f_0 : Lean.Syntax) => { stx := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instToBinarySyntax_docGen4_1 : SQLite.Blob.ToBinary Lean.Doc.Data.Syntax

Equations

• DocGen4.DB.instToBinarySyntax_docGen4_1 = { serializer := DocGen4.DB.instToBinarySyntax_docGen4_1.toBinaryAux }

def DocGen4.DB.instToBinarySyntax_docGen4_1.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.Syntax

Equations

• DocGen4.DB.instToBinarySyntax_docGen4_1.toBinaryAux { category := f_0, stx := f_1 } x✝ = SQLite.Blob.ToBinary.serializer f_1 (SQLite.Blob.ToBinary.serializer f_0 x✝)

@[implicit_reducible]

instance DocGen4.DB.instFromBinarySyntax_docGen4_1 : SQLite.Blob.FromBinary Lean.Doc.Data.Syntax

Equations

• DocGen4.DB.instFromBinarySyntax_docGen4_1 = { deserializer := DocGen4.DB.instFromBinarySyntax_docGen4_1.fromBinaryAux }

def DocGen4.DB.instFromBinarySyntax_docGen4_1.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.Syntax

Equations

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

@[implicit_reducible]

instance DocGen4.DB.instToBinaryLeanBlock_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.LeanBlock

Equations

• DocGen4.DB.instToBinaryLeanBlock_docGen4 = { serializer := DocGen4.DB.instToBinaryLeanBlock_docGen4.toBinaryAux }

def DocGen4.DB.instToBinaryLeanBlock_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.LeanBlock

Equations

• DocGen4.DB.instToBinaryLeanBlock_docGen4.toBinaryAux { commands := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryLeanBlock_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.LeanBlock

Equations

• DocGen4.DB.instFromBinaryLeanBlock_docGen4 = { deserializer := DocGen4.DB.instFromBinaryLeanBlock_docGen4.fromBinaryAux }

def DocGen4.DB.instFromBinaryLeanBlock_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.LeanBlock

Equations

• DocGen4.DB.instFromBinaryLeanBlock_docGen4.fromBinaryAux = (fun (f_0 : Lean.Doc.DocCode) => { commands := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instToBinaryLeanTerm_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.LeanTerm

Equations

• DocGen4.DB.instToBinaryLeanTerm_docGen4 = { serializer := DocGen4.DB.instToBinaryLeanTerm_docGen4.toBinaryAux }

def DocGen4.DB.instToBinaryLeanTerm_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.LeanTerm

Equations

• DocGen4.DB.instToBinaryLeanTerm_docGen4.toBinaryAux { term := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instFromBinaryLeanTerm_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.LeanTerm

Equations

• DocGen4.DB.instFromBinaryLeanTerm_docGen4 = { deserializer := DocGen4.DB.instFromBinaryLeanTerm_docGen4.fromBinaryAux }

def DocGen4.DB.instFromBinaryLeanTerm_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.LeanTerm

Equations

• DocGen4.DB.instFromBinaryLeanTerm_docGen4.fromBinaryAux = (fun (f_0 : Lean.Doc.DocCode) => { term := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

def DocGen4.DB.instToBinarySetOption_docGen4.toBinaryAux : SQLite.Blob.Serializer Lean.Doc.Data.SetOption

Equations

• DocGen4.DB.instToBinarySetOption_docGen4.toBinaryAux { term := f_0 } x✝ = SQLite.Blob.ToBinary.serializer f_0 x✝

@[implicit_reducible]

instance DocGen4.DB.instToBinarySetOption_docGen4 : SQLite.Blob.ToBinary Lean.Doc.Data.SetOption

Equations

• DocGen4.DB.instToBinarySetOption_docGen4 = { serializer := DocGen4.DB.instToBinarySetOption_docGen4.toBinaryAux }

def DocGen4.DB.instFromBinarySetOption_docGen4.fromBinaryAux : SQLite.Blob.Deserializer Lean.Doc.Data.SetOption

Equations

• DocGen4.DB.instFromBinarySetOption_docGen4.fromBinaryAux = (fun (f_0 : Lean.Doc.DocCode) => { term := f_0 }) <$> SQLite.Blob.FromBinary.deserializer

@[implicit_reducible]

instance DocGen4.DB.instFromBinarySetOption_docGen4 : SQLite.Blob.FromBinary Lean.Doc.Data.SetOption

Equations

• DocGen4.DB.instFromBinarySetOption_docGen4 = { deserializer := DocGen4.DB.instFromBinarySetOption_docGen4.fromBinaryAux }

def DocGen4.DB.builtinDocstringValues : DocstringValues

Equations

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