Documentation
Lean
.
Compiler
.
LCNF
.
OtherDecl
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
:
Name
)
(
us
:
List
Level
:=
[
]
)
:
CompilerM
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