Documentation
Lean
.
Elab
.
PreDefinition
.
Main
Search
Google site search
return to top
source
Imports
Init
Lean.Util.SCC
Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.MkInhabitant
Lean.Elab.PreDefinition.Structural
Lean.Elab.PreDefinition.WF.Main
Imported by
Lean
.
Elab
.
addPreDefinitions
source
def
Lean
.
Elab
.
addPreDefinitions
(preDefs :
Array
Lean.Elab.PreDefinition
)
:
Lean.Elab.TermElabM
Unit
Equations
One or more equations did not get rendered due to their size.
Instances For