Documentation
Lean
.
Elab
.
PreDefinition
.
WF
.
Fix
Search
Google site search
Lean
.
Elab
.
PreDefinition
.
WF
.
Fix
source
Imports
Init
Lean.Elab.RecAppSyntax
Lean.Meta.CasesOn
Lean.Util.HasConstCache
Lean.Elab.PreDefinition.Basic
Lean.Elab.Tactic.Basic
Lean.Meta.Match.Match
Lean.Meta.Tactic.Cleanup
Lean.Elab.PreDefinition.Structural.BRecOn
Lean.Elab.PreDefinition.Structural.Basic
Lean.Meta.Tactic.Simp.Main
Imported by
Lean
.
Elab
.
WF
.
mkFix
source
def
Lean
.
Elab
.
WF
.
mkFix
(preDef :
Lean.Elab.PreDefinition
)
(prefixArgs :
Array
Lean.Expr
)
(wfRel :
Lean.Expr
)
(decrTactic? :
Option
Lean.Syntax
)
:
Lean.Elab.TermElabM
Lean.Expr
Instances For