← Mathematical handbook

inductive Lean.Doc.DocScope : Type

• local : DocScope
• import (mods : Array Name) : DocScope

@[instance_reducible]

instance Lean.Doc.instFromDocArgDocScope : FromDocArg DocScope

Equations

• Lean.Doc.instFromDocArgDocScope = { fromDocArg := fun (v : Lean.Doc.DocArg) => Lean.Doc.instFromDocArgDocScope._private_1 v }