Documentation
Aesop
.
Script
.
Util
Search
return to top
source
Imports
Init
Aesop.Util.Basic
Aesop.Util.EqualUpToIds
Batteries.Lean.Meta.SavedState
Imported by
Aesop
.
Script
.
findFirstStep?
Aesop
.
Script
.
matchGoals
Aesop
.
Script
.
matchGoals
.
getProperGoals
source
@[specialize #[]]
def
Aesop
.
Script
.
findFirstStep?
{
α
β
:
Type
}
(
goals
:
Array
α
)
(
step?
:
α
→
Option
β
)
(
stepOrder
:
β
→
Nat
)
:
Option
(
Nat
×
α
×
β
)
Equations
Instances For
source
def
Aesop
.
Script
.
matchGoals
(
postState₁
postState₂
:
Lean.Meta.SavedState
)
(
goals₁
goals₂
:
Array
Lean.MVarId
)
:
Lean.MetaM
(
Option
(
Std.HashMap
Lean.MVarId
Lean.MVarId
)
)
Equations
Instances For
source
def
Aesop
.
Script
.
matchGoals
.
getProperGoals
(
state
:
Lean.Meta.SavedState
)
(
goals
:
Array
Lean.MVarId
)
:
Lean.MetaM
(
Array
Lean.MVarId
)
Equations
Instances For