HepLean Documentation
Lean
.
Compiler
.
LCNF
.
OtherDecl
Search
Google site search
return to top
source
Imports
Lean.Compiler.LCNF.BaseTypes
Lean.Compiler.LCNF.MonoTypes
Imported by
Lean
.
Compiler
.
LCNF
.
getOtherDeclType
source
def
Lean
.
Compiler
.
LCNF
.
getOtherDeclType
(declName :
Lean.Name
)
(us :
List
Lean.Level
:=
[]
)
:
Lean.Compiler.LCNF.CompilerM
Lean.Expr
Return the LCNF type for constructors, inductive types, and foreign functions.
Equations
One or more equations did not get rendered due to their size.
Instances For