- options : Options'
- ruleSet : LocalRuleSet
- normSimpContext : NormSimpContext
Instances For
- forwardState : ForwardState
- forwardRuleMatches : ForwardRuleMatches
Instances For
def
Aesop.updateForwardState
(fs : ForwardState)
(newMatches : Array ForwardRuleMatch)
(erasedHyps : Std.HashSet Lean.FVarId)
:
Equations
Instances For
- succeeded (goal : Lean.MVarId) (steps? : Option (Array Script.LazyStep)) : NormRuleResult
- proved (steps? : Option (Array Script.LazyStep)) : NormRuleResult
Instances For
Equations
Instances For
@[always_inline]
Equations
Instances For
def
Aesop.withNormTraceNode.fmt
(ruleName : DisplayRuleName)
(r : Except Lean.Exception (Option NormRuleResult))
:
Equations
Instances For
def
Aesop.runNormRuleTac
(rule : NormRule)
(input : RuleTacInput)
(fs : ForwardState)
(rs : LocalRuleSet)
:
On success, returns the rule tactic's result, the new forward state and the
new forward rule matches. If rule
corresponds to some forward rule matches,
returns the matches as well.
Equations
Instances For
def
Aesop.runNormRuleTac.err
(rule : NormRule)
(input : RuleTacInput)
{α : Type}
(msg : Lean.MessageData)
:
Equations
Instances For
def
Aesop.runNormRule
(goal : Lean.MVarId)
(mvars : UnorderedArraySet Lean.MVarId)
(rule : IndexMatchResult NormRule)
:
Equations
Instances For
def
Aesop.runFirstNormRule
(goal : Lean.MVarId)
(mvars : UnorderedArraySet Lean.MVarId)
(rules : Array (IndexMatchResult NormRule))
:
Equations
Instances For
def
Aesop.mkNormSimpScriptStep
(preGoal : Lean.MVarId)
(postGoal? : Option Lean.MVarId)
(preState postState : Lean.Meta.SavedState)
(usedTheorems : Lean.Meta.Simp.UsedSimps)
:
Equations
Instances For
Equations
Instances For
def
Aesop.normSimpCore.addLocalRules
(goal : Lean.MVarId)
(localRules : Array LocalNormSimpRule)
(ctx : Lean.Meta.Simp.Context)
(simprocs : Lean.Meta.Simp.SimprocsArray)
(isSimpAll : Bool)
:
Equations
Instances For
@[always_inline]
def
Aesop.checkSimp
(name : String)
(mayCloseGoal : Bool)
(goal : Lean.MVarId)
(x : NormM (Option NormRuleResult))
:
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
- proved (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormSeqResult
- changed (goal : Lean.MVarId) (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormSeqResult
- unchanged : NormSeqResult