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.

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 (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.

@[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]