def Aesop.RuleTac.makeForwardHyps (e : Lean.Expr) (patSubst? : Option Substitution) (immediate : UnorderedArraySet PremiseIndex) (maxDepth? : Option Nat) (forwardHypData : ForwardHypData) (existingHypTypes : Lean.PHashSet RPINF) : BaseM (Array (Lean.Expr × Nat) × Array Lean.FVarId)

Equations

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

partial def Aesop.RuleTac.makeForwardHyps.loop (maxDepth? : Option Nat) (forwardHypData : ForwardHypData) (existingHypTypes : Lean.PHashSet RPINF) (app : Lean.Expr) (instMVars immediateMVars : Array Lean.MVarId) (i : Nat) (proofsAcc : Array (Lean.Expr × Nat)) (currentMaxHypDepth : Nat) (currentUsedHyps usedHypsAcc : Array Lean.FVarId) (proofTypesAcc : Std.HashSet RPINF) : BaseM (Array (Lean.Expr × Nat) × Array Lean.FVarId × Std.HashSet RPINF)

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.assertForwardHyp.tacticBuilder (goal : Lean.MVarId) (hyp : Lean.Meta.Hypothesis) : Lean.FVarId × Lean.MVarId → Script.TacticBuilder

Equations

• Aesop.RuleTac.assertForwardHyp.tacticBuilder goal hyp x✝ = Aesop.Script.TacticBuilder.assertHypothesis goal hyp Lean.Meta.TransparencyMode.reducible

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

Equations

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

def Aesop.RuleTac.applyForwardRule.err (e : Lean.Expr) {α : Type} : Lean.MetaM α

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.forwardMatch (m : ForwardRuleMatch) : RuleTac

Equations

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