structure Aesop.RuleTac.ForwardM.Context : Type

• maxDepth? : Option Nat
• forwardHypData : ForwardHypData

@[instance_reducible]

instance Aesop.RuleTac.ForwardM.instInhabitedContext : Inhabited Context

Equations

• Aesop.RuleTac.ForwardM.instInhabitedContext = { default := Aesop.RuleTac.ForwardM.instInhabitedContext.default }

structure Aesop.RuleTac.ForwardM.State : Type

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

@[instance_reducible]

instance Aesop.RuleTac.ForwardM.instInhabitedState : Inhabited State

Equations

• Aesop.RuleTac.ForwardM.instInhabitedState = { default := Aesop.RuleTac.ForwardM.instInhabitedState.default }

@[reducible, inline]

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

Equations

• Aesop.RuleTac.ForwardM = ReaderT Aesop.RuleTac.ForwardM.Context (StateRefT' IO.RealWorld Aesop.RuleTac.ForwardM.State Aesop.ScriptM)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Aesop.RuleTac.makeForwardHypProofs' e patSubsts? immediate = Aesop.RuleTac.makeForwardHypProofs e none immediate

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.RuleTac.forwardConst decl immediate clear input = do let e ← liftM (Lean.Meta.mkConstWithFreshMVarLevels decl) Aesop.RuleTac.forwardExpr e immediate clear input

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.RuleTac.forward (Aesop.RuleTerm.const decl) immediate clear = Aesop.RuleTac.forwardConst decl immediate clear
• Aesop.RuleTac.forward (Aesop.RuleTerm.term tm) immediate clear = Aesop.RuleTac.forwardTerm tm immediate clear

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.RuleTac.forwardMatch m = Aesop.RuleTac.forwardMatches #[m]