Documentation
Lean
.
Elab
.
PreDefinition
.
Main
Search
Google site search
Lean
.
Elab
.
PreDefinition
.
Main
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
.
TerminationHints
Lean
.
Elab
.
instInhabitedTerminationHints
Lean
.
Elab
.
addPreDefinitions
source
structure
Lean
.
Elab
.
TerminationHints
:
Type
terminationBy? :
Option
Lean.Syntax
decreasingBy? :
Option
Lean.Syntax
Instances For
source
instance
Lean
.
Elab
.
instInhabitedTerminationHints
:
Inhabited
Lean.Elab.TerminationHints
source
def
Lean
.
Elab
.
addPreDefinitions
(preDefs :
Array
Lean.Elab.PreDefinition
)
(hints :
Lean.Elab.TerminationHints
)
:
Lean.Elab.TermElabM
Unit
Instances For