structure Aesop.RuleTac.ForwardM.Context : Type

• maxDepth? : Option Nat
• forwardHypData : ForwardHypData

def Aesop.RuleTac.ForwardM.instInhabitedContext.default : Context

@[implicit_reducible]

instance Aesop.RuleTac.ForwardM.instInhabitedContext : Inhabited Context

structure Aesop.RuleTac.ForwardM.State : Type

• toAssert : Array (Lean.Expr × Lean.Expr × Nat)
• usedHyps : Std.HashSet Lean.FVarId

@[implicit_reducible]

instance Aesop.RuleTac.ForwardM.instInhabitedState : Inhabited State

def Aesop.RuleTac.ForwardM.instInhabitedState.default : State

@[reducible, inline]

abbrev Aesop.RuleTac.ForwardM (α : Type) : Type

def Aesop.RuleTac.makeForwardHypProofs (e : Lean.Expr) (patSubst? : Option Substitution) (immediate : UnorderedArraySet PremiseIndex) : ForwardM Unit

def Aesop.RuleTac.makeForwardHypProofs' (e : Lean.Expr) (patSubsts? : Option (Array Substitution)) (immediate : UnorderedArraySet PremiseIndex) : ForwardM Unit

def Aesop.RuleTac.assertForwardHyp (goal : Lean.MVarId) (hyp : Lean.Meta.Hypothesis) (depth : Nat) : ScriptM (Lean.FVarId × Lean.MVarId)

def Aesop.RuleTac.applyForwardRule (goal : Lean.MVarId) (e : Lean.Expr) (patSubsts? : Option (Array Substitution)) (immediate : UnorderedArraySet PremiseIndex) (clear : Bool) (maxDepth? : Option Nat) : ScriptM Subgoal

@[inline]

def Aesop.RuleTac.forwardExpr (e : Lean.Expr) (immediate : UnorderedArraySet PremiseIndex) (clear : Bool) : RuleTac

def Aesop.RuleTac.forwardConst (decl : Lean.Name) (immediate : UnorderedArraySet PremiseIndex) (clear : Bool) : RuleTac

def Aesop.RuleTac.forwardTerm (stx : Lean.Term) (immediate : UnorderedArraySet PremiseIndex) (clear : Bool) : RuleTac

def Aesop.RuleTac.forward (t : RuleTerm) (immediate : UnorderedArraySet PremiseIndex) (clear : Bool) : RuleTac

def Aesop.RuleTac.forwardMatches (ms : Array ForwardRuleMatch) : RuleTac

def Aesop.RuleTac.forwardMatch (m : ForwardRuleMatch) : RuleTac