Documentation
Aesop
.
Util
.
Tactic
.
Ext
Search
return to top
source
Imports
Init
Aesop.Tracing
Imported by
Aesop
.
ExtResult
Aesop
.
straightLineExt
Aesop
.
straightLineExtProgress
source
structure
Aesop
.
ExtResult
:
Type
depth :
Nat
commonFVarIds :
Array
Lean.FVarId
goals :
Array
(
Lean.MVarId
×
Array
Lean.FVarId
)
Instances For
source
def
Aesop
.
straightLineExt
(
goal
:
Lean.MVarId
)
:
Lean.MetaM
ExtResult
Equations
Instances For
source
def
Aesop
.
straightLineExtProgress
(
goal
:
Lean.MVarId
)
:
Lean.MetaM
ExtResult
Equations
Instances For