Documentation
DocGen4
.
Process
.
ClassInfo
Search
return to top
source
Imports
Init
Lean
DocGen4.Process.Base
DocGen4.Process.InductiveInfo
DocGen4.Process.NameInfo
DocGen4.Process.StructureInfo
Imported by
DocGen4
.
Process
.
ClassInfo
.
ofInductiveVal
DocGen4
.
Process
.
ClassInductiveInfo
.
ofInductiveVal
source
def
DocGen4
.
Process
.
ClassInfo
.
ofInductiveVal
(
v
:
Lean.InductiveVal
)
:
Lean.MetaM
ClassInfo
Equations
DocGen4.Process.ClassInfo.ofInductiveVal
v
=
DocGen4.Process.StructureInfo.ofInductiveVal
v
Instances For
source
def
DocGen4
.
Process
.
ClassInductiveInfo
.
ofInductiveVal
(
v
:
Lean.InductiveVal
)
:
Lean.MetaM
ClassInductiveInfo
Equations
DocGen4.Process.ClassInductiveInfo.ofInductiveVal
v
=
DocGen4.Process.InductiveInfo.ofInductiveVal
v
Instances For